proposition: Lemma var_bound_spec' Gamma M t : type_assignment Gamma M t -> type_assignment (map (fun i => match nth_error Gamma i with Some phi => phi | None => (atom 0, nil) end) (seq 0 (var_bound M))) M t.
proof: Proof. move=> /type_assignment_ren_fv => /(_ _ id). rewrite ren_id_term. apply. apply: allfv_impl (var_bound_spec M) => x ?. move=> > /(@nth_error_split ty) [Gamma1] [Gamma2] [-> ?]. subst x. rewrite nth_error_map nth_error_seq /=; first done. by rewrite nth_error_app2 ?Nat.sub_diag. Qed.
imports: Undecidability.IntersectionTypes(CD Util.CD_facts) Undecidability.LambdaCalculus.Util.term_facts List PeanoNat Lia ssreflect