| ⊢ | f ⊃ empty ∨ f1 ⇒ ⊢ f ; g ⊃ g ∨ (f1 ; g) | EmptyOrNextChopImpRule |
Proof:
1 | ⊢ f ⊃empty ∨ f1 | given |
2 | ⊢ f ; g ⊃ (empty ∨ f1) ; g | |
3 | ⊢ (empty ∨ f1) ; g ≡ g ∨ (f1 ; g) | |
4 | ⊢ f ; g ⊃ g ∨ (f1 ; g) |
qed
The following an analogous special case of EmptyOrChopEqvRule: