proposition: Lemma oclause_to_wP e bc : holds e (odnf_to_oform (oclause_neq_leq_elim bc)) <-> holds e (odnf_to_oform (map w_to_oclause (oclause_to_w bc))).
proof: Proof. rewrite /oclause_to_w /oclause_neq_leq_elim. move: (@oclause_leq_elim4 bc). elim: (oclause_leq_elim bc) => [| t1 l1 ih1] //= h4. rewrite !map_cat !odnf_to_oform_cat. rewrite -[holds e (_ \/ _)]/(holds e _ \/ holds e _). suff <- : (oclause_neq_elim t1) = map w_to_oclause [seq (let: Oclause eq_l _ lt_l _ := x in (eq_l, lt_l)) | x <- oclause_neq_elim t1]. by rewrite ih1 // => - oc hoc; apply: h4; rewrite in_cons hoc orbT. have : forall oc, oc \in (oclause_neq_elim t1) -> oc.2 = [::] /\ oc.4 = [::]. move=> oc hoc; move/oclause_neq_elim2: (hoc); case/andP=> /eqP -> /eqP ->. by move/eqP: (h4 _ (mem_head _ _))->. elim: (oclause_neq_elim t1) => [| [teq1 tneq1 tleq1 tlt1] l2 ih2] h24 //=. rewrite /w_to_oclause /=; move: (h24 _ (mem_head _ _ ))=> /= [] -> ->. by congr (_ :: _); apply: ih2 => oc hoc; apply: h24; rewrite in_cons hoc orbT. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)