ChopPlusImpCS

⊢ f+ ⊃ f∗ ChopPlusImpCS

Proof:

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

qed

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