proposition: Lemma eq_prover_thy : forall thy up P Q, eq_prover P Q -> eq_prover (prover_thy P thy up) (prover_thy Q thy up).
proof: Proof. unfold eq_prover, prover_thy. intros. destruct up; try reflexivity. unfold run_thy_prover. destruct (thy (hconsmap st) (generate_conflict_clause st g)); auto. destruct p. destruct_in_goal M1; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause