LeftYieldsEqvYields

f f1 ⇒ ⊢ (f g) (f1 g) LeftYieldsEqvYields

Proof:

1
f f1
given
2
f ; ¬g f1 ; ¬g
3
⊢ ¬(f ; ¬g) ≡¬(f1 ; ¬g)
2,Prop
4
f g f1 g
3, def. of 

qed

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023