proposition: Lemma type_assignment_weaken_assumption s phi s' phi' Gamma1 Gamma2 M t : incl (s :: phi) (s' :: phi') -> type_assignment (Gamma1 ++ (s, phi) :: Gamma2) M t -> type_assignment (Gamma1 ++ (s', phi') :: Gamma2) M t.
proof: Proof. move=> H. apply: type_assignment_weaken. elim: Gamma1. - move=> [|?] /= >. + move=> [<- <-] /H ?. by do 2 eexists. + by eauto. - move=> [??] > IH [|?] > /=. + move=> [<- <-] ?. by do 2 eexists. + by eauto. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect