proposition: Lemma beval_clauses_one_var : forall p cls, (forall env : HFormula -> bool, beval_cnf env cls = true -> env p = true) -> (forall v , is_var_of_cnf v cls -> p = v) -> exists cl, In cl cls /\ forall l, In l cl -> l = POS p.
proof: Proof. intros. specialize (H (fun _ => false)). induction cls. - simpl in *. intuition congruence. - simpl in *. destruct (beval_clause (fun _ => false) a) eqn:B. simpl in H. apply IHcls in H. destruct H as (cl & IN & ALLPOS). exists cl. tauto. { intros. apply H0. rewrite is_var_of_cnf_cons. tauto. } simpl in H. clear H. assert (IVC : forall v, is_var_of_clause v a -> p = v). { intros. apply H0. rewrite is_var_of_cnf_cons. tauto. } specialize (beval_clause_one_var p _ IVC B). intros. exists a. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause