proposition: Lemma SN {Gamma P t} : typing Gamma P t -> sn P.
proof: Proof. intros Htp. pose proof (fundamental Htp poly_var var (fun _ _ => False)). asimpl in H. eapply R_sn, H. intros n. eapply R_var. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms