| ⊢ | empty ⊃ g, ⊢ (f ∧more) ; g ⊃ g ⇒ ⊢ f∗ ⊃ g | CSElim |
Proof:
1 | ⊢ f∗≡empty ∨ (f ∧more) ; f∗ | |
2 | ⊢ empty ⊃ 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