proposition: Lemma cons_lit_twice : forall env a l, eval_lit env a (eval_clause env (cons_lit a l)) <-> eval_clause env (cons_lit a l).
proof: Proof. induction l; simpl. - unfold eval_lit. destruct a; simpl. tauto. tauto. - destruct a0; simpl. unfold eval_lit. destruct a; simpl. tauto. tauto. destruct (pol a) eqn:A; simpl. unfold eval_lit. rewrite A. simpl. destruct a; try discriminate. simpl. unfold eval_lit in IHl. simpl in *. tauto. unfold eval_lit. simpl. rewrite A. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause