proposition: Lemma prover_rew : forall thy up n, prover thy up (n:nat) = match n with | O => fun _ _ => Fail OutOfFuel | S n => let ProverTRec := prover thy up n in seq_prover (prover_unit_propagation n) (seq_prover (prover_case_split ProverTRec) (seq_prover (prover_impl_arrows ProverTRec) (prover_thy ProverTRec thy up))) end.
proof: Proof. destruct n ; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause