proposition: Lemma beval_clause_one_var : forall p cl, (forall v, is_var_of_clause v cl -> p = v) -> beval_clause (fun _ => false) cl = false -> (forall l, In l cl -> l = POS p).
proof: Proof. intros. induction cl. - simpl in *. tauto. - simpl in *. rewrite orb_false_iff in *. destruct H0 ; subst. intros. destruct H1 ; subst. + assert (p = (var l)). { apply H. unfold is_var_of_clause. simpl. exists l. intuition congruence. } subst. destruct l ; simpl in *; auto. unfold beval_lit in *. simpl in *. discriminate. + eapply IHcl; eauto. intros. apply H. rewrite is_var_of_clause_cons. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause