Theorem: not_mem_free_of_subst (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 s
⊢ v ∉ free (t[v := s])
Tactic:
rw [free_subst_eq]
State after:
α : 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 s
⊢ v ∉ free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}

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 s
⊢ v ∉ free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
simp_all
State after:
no goals