| ⊢ | f ∧more ⊃ (g ∧more) ; f ⇒ ⊢ f ⊃ g∗ | CSIntro |
Proof:
1 | ⊢ f ∧more ⊃ (g ∧more) ; f | given |
2 | ⊢ more ≡¬empty | |
3 | ⊢ f ∧¬empty ⊃ (g ∧more) ; f | |
4 | ⊢ g∗≡empty ∨ (g ∧more) ; g∗ | |
5 | ⊢ f ∧¬g∗⊃ (g ∧more) ; f ∧¬((g ∧more) ; g∗) | |
6 | ⊢ g ∧more ⊃more | |
7 | ⊢ f ⊃ g∗ |
qed