| ⊢ | w ∧ (f ; g) ≡ ( w ∧ f) ; ( w ∧ g) | BoxStateAndChopEqvChop |
Proof for ⊃ :
1 | ⊢ w ≡ w | |
2 | ⊢ w ∧ (f ; g) ⊃ ( w ∧ f) ; ( w ∧ g) |
qed
Proof for ⊂:
1 | ⊢ ( w ∧ f) ; ( w ∧ g) ⊃ ( w) ; ( w ∧ g) | |
2 | ⊢ ( w) ; ( w ∧ g) ⊃ ( w) ; ( w) | |
3 | ⊢ ( w) ; ( w) ≡ w | |
4 | ⊢ ( w ∧ f) ; ( w ∧ g) ⊃ f ; ( w ∧ g) | |
5 | ⊢ f ; ( w ∧ g) ⊃ f ; g | |
6 | ⊢ ( w ∧ f) ; ( w ∧ g) ⊃ w ∧ (f ; g) |
qed
See also the lemma BoxStateAndCSEqvCS for chop-star.