proposition: Lemma type_assignment_mergeL Delta Gamma M t : type_assignment Gamma M t -> type_assignment (merge Delta Gamma) M t.
proof: Proof. apply: type_assignment_weaken. elim: Delta Gamma. - move=> /= > -> ?. by do 3 econstructor. - move=> [??] > IH [|[??] ?] /=. + by case. + move=> [|?] /=. * move=> > [] *. subst. do 3 econstructor; [done|]. right. apply /in_app_iff. by right. * by apply: IH. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect