- by negate_fun we proved (negate F1 ≡ negate F2) (H1).
- by not_dualize_eq_negate, equiv_rewrite we proved (FNot (dualize F1) ≡ negate F2) (H2).
- by not_dualize_eq_negate, equiv_rewrite we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
- by not_inj we proved (dualize F1 ≡ dualize F2) (H4).
+ by (*BEGIN*)negate_fun(*END*) we proved (negate F1 ≡ negate F2) (H1).
+ by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2).
+ by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
+ by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4).