Narrow

lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) :    Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := by  generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der  induction der generalizing Γ  case var X' _ _ =>    grind [Env.Wf.narrow, List.perm_nodupKeys, => List.perm_dlookup]  case' abs  => apply abs (free_union Var)  case' tabs => apply tabs (free_union Var)  case' let' der _ => apply let' (free_union Var) (der eq)  case' case der _ _ => apply case (free_union Var) (der eq)  all_goals grind [Ty.Wf.narrow, Env.Wf.narrow, Sub.narrow]