proposition: Lemma type_assignment_weaken Gamma Delta M t : (forall n t s phi, nth_error Gamma n = Some (s, phi) -> In t (s :: phi) -> exists s' phi', nth_error Delta n = Some (s', phi') /\ In t (s' :: phi')) -> type_assignment Gamma M t -> type_assignment Delta M t.
proof: Proof. elim: M Gamma Delta t. - move=> > H /type_assignmentE [] > /H /[apply] - [?] [?] [??]. by econstructor; eassumption. - move=> ? IH1 ? IH2 > H /type_assignmentE [] >. move: (H) => /IH1 /[apply] ?. move: (H) => /IH2 /[apply] ? H'. econstructor; [eassumption..|]. apply: Forall_impl H' => ? /IH2. by apply. - move=> ? IH ?? [|??] > H /type_assignmentE; [done|]. move=> /IH {}IH. constructor. apply: IH. move=> [|?] >; [|by apply: H]. move=> /= [] *. subst. by do 3 econstructor. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect