proposition: Lemma cnf_correct_list : forall m l (WF: Forall (has_form m) l) (H : forall x : t LForm, In x l -> forall (pol : bool) (g : option HFormula) (cp cm : IntMap.ptrie unit) (ar : list literal) (acc : list watched_clause) (hf : t LForm), has_form m hf -> elt hf = elt x -> ((Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g) -> (Forall eval_watched_clause (snd (cnf pol (is_classic g) cp cm ar acc (elt x) hf)) -> eval_ohformula g) -> eval_ohformula g) (g : option HFormula) pol (acc : list watched_clause) (hf : t LForm), forall (ar : list literal) (acc' : list watched_clause) (ACC' : (Forall eval_watched_clause acc' -> eval_ohformula g) -> eval_ohformula g), forall cm' cp' : IntMap.ptrie unit, (Forall eval_watched_clause (snd (cnf_list cnf pol (is_classic g) cp' cm' ar acc' l)) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. intros. revert cm' cp' ar acc' ACC' H0. induction l; simpl. * auto. * intros cm' cp' ar acc' ACC' . destruct (cnf pol (is_classic g) cp' cm' ar acc' (elt a) a) as (((cp1,cm1),ar1),acc1) eqn:EQPf1. rewrite Forall_rew in WF. apply IHl; auto. tauto. intros. revert H4. apply H;auto. simpl. tauto. change acc1 with (snd (cp1,cm1,ar1,acc1)). rewrite <- EQPf1. apply H; auto. simpl. tauto. tauto. Defined.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause