proposition: Lemma prover_intro_correct : forall st, sound_prover prover_intro st.
proof: Proof. repeat intro. unfold prover_intro in PRF. destruct g; try congruence. assert (WF := wf_intro_state (elt h) st h eq_refl HASF WFS). assert (HM := hconsmap_intro_state st (elt h) h). destruct (intro_state st (elt h) h) eqn:EQ; try congruence. - destruct r. inv PRF. simpl in *. split_and; intros. + apply intro_state_correct_None in EQ; auto. + eapply eval_annot_intro_state;eauto. rewrite EQ ;auto. + constructor. + rewrite HM ; auto with wf. + constructor. + auto. - destruct st0 as (st',g'). destruct WF as (WF' & HF). destruct (ProverTCorrect _ _ _ _ _ WF' HF PRF) as (P1 & P2 & P3 & P4 & P5 & P6). split_and; auto. + intros. apply intro_state_correct_Some in EQ; auto. + intros. eapply eval_annot_intro_state;eauto. rewrite EQ ;auto. + simpl in *. rewrite <- HM by auto. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause