| ⊢ | f ⊃ g ; f, ⊢ g ⊃ more ⇒ ¬f | ChopLoop |
Proof:
1 | ⊢ f ⊃ g ; f | given |
2 | ⊢ g ⊃more | given |
3 | ⊢ g ; f ⊃more ; f | |
4 | ⊢ f ⊃more ; f | |
5 | ⊢ ¬f |
qed
Here is a variant of lemma MoreChopContra that is useful in proofs: