proposition: Lemma type_preservation {Gamma t M N} : steps M N -> type_assignment Gamma M t -> type_assignment Gamma N t.
proof: Proof. elim; by eauto using type_preservation_step with nocore. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect