proposition: Lemma sn_app_var M x : sn (app M (var x)) -> sn M.
proof: Proof. by move=> /snE []. 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