proposition: Lemma typing_normal_form_poly_absE {Gamma P t}: normal_form P -> typing Gamma P (poly_abs t) -> forall x, exists Q, normal_form Q /\ term_size Q <= term_size P + 2 /\ typing Gamma Q (ren_poly_type (x .: id) t).
proof: Proof. case. - move=> {}P ? HP x. exists (ty_app P (poly_var x)). constructor; first by eauto using normal_form, head_form. constructor; first by move=> /=; lia. move: HP => /typing_ty_app => /(_ (poly_var x)). congr typing. rewrite -[RHS]subst_poly_type_poly_var ?poly_type_norm. apply: ext_poly_type. by case. - by move=> > ? /typingE [?] []. - move=> {}P ? /typingE [?] [[<-]] + x. move=> /(typing_ren_poly_type (x .: id)) HP. exists (ren_term (x .: id) id P). constructor; first by apply: normal_form_ren_term. rewrite term_size_ren_term /=. constructor; first by lia. move: HP. congr typing. rewrite map_map -[RHS]map_id. apply: map_ext. move=> ?. by rewrite ?poly_type_norm ren_poly_type_id'. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun