proposition: Lemma pure_typing_many_pure_term_absE {Gamma n M t}: pure_typing Gamma (many_pure_term_abs n M) t -> exists (nss : list (nat * poly_type)) t', n = length nss /\ t = fold_right (fun '(n, s) r => many_poly_abs n (poly_arr s r)) t' nss /\ pure_typing (fold_left (fun Gamma '(n, s) => s :: map (ren_poly_type (Nat.add n)) Gamma) nss Gamma) M t'.
proof: Proof. elim: n Gamma t; first by move=> Gamma t /= HM; exists [], t. move=> n IH Gamma t /= /pure_typingE [n1] [s1] [t1] [+] ->. move=> /IH [nss] [t'] [->] [->] HM. by exists ((n1, s1) :: nss), t'. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts pure_typing_facts) ssreflect ssrbool ssrfun