proposition: Lemma eval_clause_cons_lit_tauto : forall (env: HFormula -> Prop) p l, env p -> eval_clause env (cons_lit (POS p) l).
proof: Proof. induction l;simpl. - unfold eval_lit. simpl. tauto. - rewrite orb_false_r. destruct (pol a). simpl. unfold eval_lit. simpl. destruct (pol a). tauto. tauto. simpl. intros. destruct a; unfold eval_lit; simpl. tauto. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause