proposition: Lemma typing_normal_form_poly_arrE {Gamma P s t}: normal_form P -> typing Gamma P (poly_arr s t) -> exists Q, normal_form Q /\ term_size Q <= term_size P + 2 /\ typing (s :: Gamma) Q t.
proof: Proof. case. - move=> {}P HP. move=> /(@typing_ren_term' S) => /(_ (s :: Gamma) ltac:(done)) H. exists (app (ren_term id S P) (var 0)). constructor; last constructor. + apply: normal_form_head_form. apply: head_form_app; [by apply: head_form_ren_term | by eauto using normal_form, head_form ]. + rewrite /= term_size_ren_term. by lia. + apply: typing_app; [by eassumption | by apply: typing_var]. - move=> > ? /typingE [?] [[-> ->]] ?. eexists. constructor; first by eassumption. move=> /=. constructor; [by lia | done]. - by move=> ? ? /typingE [?] []. 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