proposition: Lemma eq_prover_impl_arrows : forall P Q, eq_prover P Q -> eq_prover (prover_impl_arrows P) (prover_impl_arrows Q).
proof: Proof. unfold eq_prover. unfold prover_impl_arrows. intros. revert g. generalize (find_arrows st (arrows st)). intro l; revert st. induction l; simpl. reflexivity. intros. destruct (intro_state (remove_arrow a st) (elt (form_of_literal a)) (form_of_literal a)); try reflexivity. destruct f; try reflexivity. apply IHl; auto. apply IHl; auto. destruct r; try reflexivity. destruct_in_goal M1; try reflexivity. auto. destruct st0. rewrite H. destruct (Q s o); try reflexivity. destruct f; auto. destruct r,p. destruct_in_goal M1; try reflexivity. auto. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause