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