| ⊢ | g ≡ g1 ⇒ ⊢ f ; g ≡ f ; g1 | RightChopEqvChop |
Proof:
1 | ⊢ g ≡ g1 | given |
2 | ⊢ g ⊃ g1 ⇒ ⊢ f ; g ⊃ f ; g1 | |
3 | ⊢ g1 ⊃ g ⇒ ⊢ f ; g1 ⊃ f ; g | |
4 | ⊢ g ≡ g1 ⇒ ⊢ f ; g ≡ f ; g1 | 2, 3 |
qed