proposition: Lemma spec_same_level : forall A (P:Z->Z->A->Prop) (f : forall n, dom_t n -> dom_t n -> A), (forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)) -> forall x y, P [x] [y] (same_level f x y).
proof: Proof. intros. apply spec_same_level_dep with (P:=fun _ => P); auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen