Theorem: free_subst_of_not_free (LambdaCalculi/TypeSystem.lean)

State before:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free t
⊢ free (t[v := s]) = free t
Tactic:
rw [subst_eq_of_not_free h]
State after:
no goals