Soundness

lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) : entails Γ t τ := by  induction derivation_t with  | var Γ xσ_mem_Γ => grind  | @abs σ Γ t τ L HL IH =>    intro E _ _ s    have sat_semMap_σ := semanticMap_saturated (Var := Var) σ    have sat_semMap_τ := semanticMap_saturated (Var := Var) τ    have := sat_semMap_τ.multiApp (multiSubst E t) s []    let := multiSubst E t    have ⟨x, _⟩ := fresh_exists <| E.dom ∪ free_union [fv, Context.dom, Env.fv] Var    have := IH (x := x) (E := ⟨x,s⟩ :: E)    grind [multiSubst_abs, entailsContext_cons, multiSubst_open_var]  | app => grind [multiSubst_app]