proposition: Lemma beval_cnf_normalise : forall env cl, beval_cnf env (map_filter Elim.normalise cl) = beval_cnf env cl.
proof: Proof. induction cl. - simpl. tauto. - simpl. specialize (beval_normalise env a). destruct (Elim.normalise a). simpl. intro. rewrite <- H. rewrite IHcl. reflexivity. simpl. intros. rewrite H. simpl. auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause