proposition: Lemma empty_thy : forall (is_dec: int -> bool) (eA: int -> Prop), Thy is_dec eA empty_thy_prover.
proof: Proof. unfold Thy, empty_thy_prover. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause