| ⊢ | ¬f ≡ f more | NotEqvYieldsMore |
Proof:
1 | ⊢ f ; empty ≡ f | |
2 | ⊢ ¬(f ; empty) ≡¬f | |
3 | ⊢ empty ≡¬more | def. of empty |
4 | ⊢ f ; empty ≡ f ; ¬more | |
5 | ⊢ ¬(f ; empty) ≡¬(f ; ¬more) | |
6 | ⊢ ¬f ≡¬(f ; ¬more) | |
7 | ⊢ ¬f ≡ f more | 6, def. of |
qed