proposition: Lemma encodes_natI (n: nat) : encodes_nat (poly_var (n + zt)) n.
proof: Proof. constructor; eexists; apply: typing_abs; by apply: (typing_var (x := 0)). 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