proposition: Lemma eval_annot_success : forall m g u l d (HASG : has_oform m g) (WFU : wf_units_lit u m) (HL : eval_annot eval_literal m l) (CL : check_annot has_literal m l) (WFL : Annot.lift (has_literal m) l) (SUC : success g u l = Some d) (EU : eval_annot_units u m), (eval_pset m d -> eval_ohformula g).
proof: Proof. intros. unfold success in *. destruct g; simpl. destruct (is_goalb h (Annot.elt l)) eqn:G. - simpl in HASG. inv SUC. unfold Annot.lift in *. unfold eval_annot in HL. 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. apply HL;auto. - exfalso ; eapply eval_annot_is_unsat ; eauto. - exfalso ; eapply eval_annot_is_unsat ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause