-(*
-lemma not_dualize_eq_negate : ∀F. FNot (dualize F) ≡ negate F.
-intros; intro; elim F; intros; try reflexivity;
-[1,2: simplify in ⊢ (? ? ? %); rewrite <(H); rewrite <(H1);
- [rewrite < (min_max (dualize f) (dualize f1) v); reflexivity;
- |rewrite < (max_min (dualize f) (dualize f1) v); reflexivity;]
-|3: change in ⊢ (? ? ? %) with [[FImpl (negate f) (negate f1)]]_v;
- change in ⊢ (? ? ? %) with (max (1 - [[negate f]]_v) [[negate f1]]_v);
- rewrite <H1; rewrite <H;
- rewrite > (max_min (FNot (dualize f)) ((dualize f1)) v);reflexivity;
-|4: simplify; rewrite < H; reflexivity;]
-qed.
-*)