| ⊢ | w ⊃ (f ≡ f1) ⇒ ⊢ w ⊃ ((f ; g) ≡ (f1 ; g)) | StateImpChopEqvChop |
Proof:
1 | ⊢ w ⊃ f ≡ f1 | given |
2 | ⊢ w ∧ f ⊃ f1 | |
3 | ⊢ w ∧ (f ; g) ⊃ (f1 ; g) | |
4 | ⊢ w ∧ f1 ⊃ f | |
5 | ⊢ w ∧ (f1 ; g) ⊃ (f ; g) | |
6 | ⊢ w ⊃ (f ; g) ≡ (f1 ; g) |
qed