Weaken

lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :    Typing (Γ ++ Θ ++ Δ) t τ := by  generalize eq : Γ ++ Δ = ΓΔ at der  induction der generalizing Γ  case' abs => apply abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)  case' tabs => apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)  case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)  case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)  all_goals    grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup]