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