| ⊢ | ¬(f ; g) ≡ f ¬g | NotChopEqvYieldsNot |
Proof:
1 | ⊢ g ≡¬¬g | |
2 | ⊢ f ; g ≡ f ; ¬¬g | |
3 | ⊢ ¬(f ; g) ≡¬(f ; ¬¬g) | |
4 | ⊢ ¬(f ; g) ≡¬(f g) | def. of |
qed
The following lemma TrueChopEqvDiamond is no longer needed since is now defined in terms of chop:
| ⊢ | true ; f ≡ f | TrueChopEqvDiamond |