EmptyYields

⊢ empty f ≡ f EmptyYields

Proof:

1
⊢ empty ; ¬f ≡¬f
2
⊢ ¬(empty ; ¬f) ≡ f
1,Prop
3
⊢ empty f ≡ f
2, def. of 

qed

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024