proposition: Lemma eq_prover_case_split_ann : forall P Q, eq_prover P Q -> forall cl d, eq_prover (case_split_ann P d cl) (case_split_ann Q d cl).
proof: Proof. unfold eq_prover, case_split_ann. intros. replace (case_split P cl st g) with (case_split Q cl st g). reflexivity. revert st g. induction cl. + reflexivity. + simpl. intros. rewrite H. destruct_in_goal G; try reflexivity. destruct r,p. destruct_in_goal C2; try reflexivity. destruct_in_goal M1; try reflexivity. rewrite IHcl. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause