proposition: Lemma sound_prover_seq : forall P Q (CP : forall st, sound_prover P st) (CPP : forall st st', sound_prover_progress P st st') (CQ : forall st, sound_prover Q st), forall st, sound_prover (seq_prover P Q) st.
proof: Proof. intros. unfold seq_prover. unfold sound_prover. intros. destruct (P st g) eqn:EQ ; try congruence. - destruct f ; try congruence. eapply CQ ; eauto. - destruct r. destruct p. inv PRF. eapply CP ; eauto. - eapply CPP in EQ ; eauto. eapply CQ in PRF. split_and; try tauto. + intuition. eapply hmap_order_trans; eauto. + tauto. + eapply has_oform_mono ; eauto. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause