proposition: Lemma prenex_Gamma_W : Forall (fun t => exists n s, t = many_poly_abs n s /\ is_simple s /\ allfv_poly_type (gt n) s) Gamma_W.
proof: Proof. apply /Forall_cons_iff. constructor. { exists 2, t_0_W. constructor; [done | constructor; [done | by move=> /=; lia ]]. } apply /Forall_cons_iff. constructor; last done. do 2 eexists. constructor; first by reflexivity. by constructor; [apply: is_simple_t_1_W | apply: closed_t_1_W ]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts pure_typable_prenex) ssreflect ssrbool ssrfun