proposition: Lemma sn_normal Γ P s : typing Γ P s -> sn P -> exists Q, clos_refl_trans _ step P Q /\ normal_form Q.
proof: Proof. intros H. induction 1 as [P Hsn IH] in s, H |- *. destruct (progress P) as [Hstep | [Q Hstep]]. - exists P. split. econstructor 2. eauto using nf_normal_form, sn_normal_form. - pose proof (Hstep' := Hstep). eapply IH in Hstep as (Q' & H1 & H2). + exists Q'. split. econstructor 3. econstructor 1. all: eauto. + eauto using preservation. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.typing_facts Undecidability.SystemF.Util.term_facts Coq.Relations.Relation_Operators Coq.Program.Equality