proposition: Lemma abs_Gamma_spec Gamma M t : type_assignment Gamma M t -> exists t', type_assignment nil (Nat.iter (length Gamma) lam M) t'.
proof: Proof. elim: Gamma M t. { move=> ???. eexists. by eassumption. } move=> [s phi] Gamma IH ?? /type_assignment_arr /IH /=. congr ex. congr type_assignment. elim: (length Gamma). { done. } by move=> ? /= ->. Qed.
imports: Undecidability.IntersectionTypes(CD Util.CD_facts) Undecidability.LambdaCalculus.Util.term_facts List PeanoNat Lia ssreflect