proposition: Lemma is_safe_poly_typeE {i t} : is_safe_poly_type i t -> exists (n : nat) (ts : list poly_type) (x : nat), t = many_poly_abs n (many_poly_arr ts (poly_var (n + (i + x)))).
proof: Proof. elim: t i. - move=> /= x i *. exists 0, [], (x-i). congr poly_var. by lia. - move=> s _ t _ ? /= /is_safe_poly_arrE [ts] [x] ->. by exists 0, (s :: ts), x. - move=> ? IH i /IH [n] [ts] [x] ->. exists (1+n), ts, x. move=> /=. do 4 f_equal. 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