proposition: Lemma is_unsat_correct : forall m lit (l:Annot.t literal) d (HL : Annot.lift (has_literal m) l) (EL : Annot.lift eval_literal l) (EU : eval_units m lit) (US : is_unsat lit l = Some d), False.
proof: Proof. unfold is_unsat. unfold Annot.lift. intros. destruct (Annot.elt l). - destruct (is_hFF f) eqn:FF. + apply is_hFF_true in FF. subst. simpl in EL ; auto. + generalize (has_form_find_lit _ _ _ HL EU). destruct (IntMap.get' (id f) lit); try congruence. unfold Annot.lift in *. destruct_in_hyp US b; try discriminate. rewrite negb_true_iff in b. rewrite b. simpl. tauto. - simpl; intros. generalize (has_form_find_lit _ _ _ HL EU). destruct (IntMap.get' (id f) lit); try congruence. unfold Annot.lift. destruct_in_hyp US b; try discriminate. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause