ImpCS

⊢ f ⊃ f∗ ImpCS

Proof:

1
⊢ f ⊃ f+
2
⊢ f ⊃empty ∨ f+
1,Prop
3
⊢ f ⊃ f∗
2, def. of ∗

qed

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