proposition: Lemma Admissible_sn : Admissible sn.
proof: Proof. constructor. - by apply: head_exp_sn. - by apply: neutal_sn_sn. - by apply: sn_app_var. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations List Wellfounded.Transitive_Closure ssreflect