proposition: Theorem fmmap_reifer_bound p n (P : nat -> (nat -> nat) -> Prop) : (forall x f g, equal_upto p f g -> P x f -> P x g) -> (forall x, x < n -> exists f, P x f) -> exists m f, forall x, x < n -> (forall j, j < p -> f x j < m) /\ P x (f x).
proof: Proof. intros H1 H2. apply fmmap_bound with (1 := H1) in H2. destruct H2 as (m & Hm). apply fmap_reifier_default in Hm; auto. destruct Hm as (f & Hf); exists m, f; auto. Qed.
imports: Arith Lia