| ⊢ | f∗∧more ≡ (f ∧more) ; f∗ | CSAndMoreEqvAndMoreChop |
Proof for ⊃ :
1 | ⊢ (empty ∨ (f ∧more) ; f∗) ∧more ⊃ (f ∧more) ; f∗ | |
2 | ⊢ f∗∧more ⊃ (f ∧more) ; f∗ | 1, def. of ∗ |
qed
Proof for ⊂:
1 | ⊢ f∗≡empty ∨ (f ∧more) ; f∗ | |
2 | ⊢ (f ∧more) ; f∗⊃ f∗ | |
3 | ⊢ (f ∧more) ; f∗⊃more | |
4 | ⊢ (f ∧more) ; f∗⊃ f∗∧more |
qed