proposition: Lemma eq_seq_prover : forall P1 P2 Q1 Q2, eq_prover P1 Q1 -> eq_prover P2 Q2 -> eq_prover (seq_prover P1 P2) (seq_prover Q1 Q2).
proof: Proof. unfold seq_prover,eq_prover. intros. rewrite H. destruct (Q1 st g); try congruence. destruct f; try reflexivity. apply H0. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause