proposition: Lemma run_thy_prover_correct : forall st, sound_prover run_thy_prover st.
proof: Proof. unfold sound_prover. intros. unfold run_thy_prover in PRF. specialize (wf_generate_conflict_clause WFS HASF). set (l := (generate_conflict_clause st g)) in * ; clearbody l. intro C. destruct (thy_prover (hconsmap st) l) eqn:THY ; try congruence. destruct p as (h',cl'). apply thy_prover_sound in THY. destruct THY as (EV & ORD & WF). generalize (set_hmap_correct h' st ORD WFS). intros (EV' & EA' & WF' & ORD'). set (st' := set_hmap h' st) in *. clearbody st'. subst. generalize (augment_with_clauses_correct cl' st' WF' WF). intros (ORD2 & WF2 & EVAL2 & EA2). unfold hconsmap_progress in ORD2. destruct (augment_with_clause cl' st'); try congruence. - destruct r. inv PRF. simpl in *. rewrite! Forall_rew. intuition. + subst. auto. + revert WF. apply ForallMono. apply has_literal_mono. subst. auto with wf. - apply ProverTCorrect in PRF; auto. simpl in *. destruct PRF as (PRF1 & PRF2 & PRF3 & PRF4 & PRF5 & PRF6). split_and ; try tauto. + eapply hmap_order_trans;eauto. rewrite <- ORD2 by tauto. auto. + revert HASF. simpl in *. apply has_oform_mono. eapply hmap_order_trans;eauto. rewrite <- ORD2 by tauto. auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause