| ⊢ | f ; f+ ⊃ f+ | ChopChopPlusImpChopPlus |
Proof:
1 | ⊢ empty ∨more | |
2 | ⊢ f ⊃empty ∨ (f ∧more) | |
3 | ⊢ f ; f+ ⊃ f+ ∨ (f ∧more) ; f+ | |
4 | ⊢ f+ ≡ f ∨ (f ∧more) ; f+ | |
5 | ⊢ (f ∧more) ; f+ ⊃ f+ | |
6 | ⊢ f ; f+ ⊃ f+ | |
qed