proposition: Lemma is_var_of_cnf_normalise : forall v l, is_var_of_cnf v (map_filter Elim.normalise l) -> is_var_of_cnf v l.
proof: Proof. induction l; simpl;auto. destruct (Elim.normalise a) eqn: N. - rewrite !is_var_of_cnf_cons. apply normalise_vars with (p:=v) in N. tauto. - rewrite is_var_of_cnf_cons. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause