proposition: Lemma prover_op_eq : forall thy use_prover n, eq_prover (prover thy use_prover n) (prover_opt thy use_prover n).
proof: Proof. unfold eq_prover. induction n. - simpl. reflexivity. - simpl. intros. unfold seq_prover at 1. unfold prover_unit_propagation. destruct (unit_propagation n g st) eqn:UP. + destruct f; try reflexivity. apply unit_propagation_not_stuck in UP. tauto. + destruct r; auto. + repeat apply eq_seq_prover. apply eq_prover_case_split;auto. apply eq_prover_impl_arrows; auto. apply eq_prover_thy;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause