proposition: Lemma ϵP (x: nat) : x < δ -> φ x <= ϵ.
proof: Proof. suff: Forall (fun x => φ x <= ϵ) (seq 0 δ). { move=> + ? => /Forall_forall. apply. apply /in_seq. by lia. } rewrite /ϵ. elim: (seq 0 δ); first by constructor. move=> {}x xs IH. constructor. - move=> /=. by lia. - apply: Forall_impl IH => ? /=. by lia. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun