proposition: Lemma success_correct : forall m g u l d (HASG : has_oform m g) (WFL : Annot.lift (has_literal m) l) (SUC : success g u l = Some d) (EU : eval_units m u) (EL : Annot.lift eval_literal l), eval_ohformula g.
proof: Proof. intros. unfold success in *. destruct g; simpl. destruct (is_goalb h (Annot.elt l)) eqn:G. - simpl in HASG. unfold Annot.lift in *. destruct (Annot.elt l) ; simpl in G ; try discriminate. assert (G2 : id f = id h) by lia. apply has_form_eq with (m:=m) in G2;auto. subst; auto. - exfalso ; eapply is_unsat_correct ; eauto. - exfalso ; eapply is_unsat_correct ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause