| ⊢ | f ⊃ g, ⊢ (f ∧more) ; g ⊃ g ⇒ ⊢ f+ ⊃ g | ChopPlusElim |
Proof:
1 | ⊢ f+ ≡ f ∨ (f ∧more) ; f+ | |
2 | ⊢ f ⊃ g | given |
3 | ⊢ (f ∧more) ; g ⊃ g | given |
4 | ⊢ f+ ∧¬g ⊃ (f ∧more) ; f+ ∧¬((f ∧more) ; g) | |
5 | ⊢ f ∧more ⊃more | |
6 | ⊢ f+ ⊃ g |
qed