Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders (FOL/NV/Sub/Var/One/Rec/ReplaceFree.lean)

State before:
F : Formula
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders F = F
Tactic:
induction F generalizing binders
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders true_ = true_

case false_
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders false_ = false_

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders a✝.not_ = a✝.not_

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = def_ a✝¹ a✝

State before:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders true_ = true_

case false_
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders false_ = false_

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders a✝.not_ = a✝.not_

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = def_ a✝¹ a✝
Tactic:
any_goals
  simp only [replaceFreeAux]
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ pred_const_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = pred_const_ a✝¹ a✝

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ pred_var_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = pred_var_ a✝¹ a✝

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ eq_ (if v = a✝¹ ∧ a✝¹ ∉ binders then t else a✝¹) (if v = a✝ ∧ a✝ ∉ binders then t else a✝) = eq_ a✝¹ a✝

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders a✝).not_ = a✝.not_

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders a✝¹).imp_ (replaceFreeAux v t binders a✝) = a✝¹.imp_ a✝

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders a✝¹).and_ (replaceFreeAux v t binders a✝) = a✝¹.and_ a✝

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders a✝¹).or_ (replaceFreeAux v t binders a✝) = a✝¹.or_ a✝

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝¹ = a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders a✝¹).iff_ (replaceFreeAux v t binders a✝) = a✝¹.iff_ a✝

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ forall_ a✝¹ (replaceFreeAux v t (binders ∪ {a✝¹}) a✝) = forall_ a✝¹ a✝

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders a✝ = a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ exists_ a✝¹ (replaceFreeAux v t (binders ∪ {a✝¹}) a✝) = exists_ a✝¹ a✝

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = def_ a✝¹ a✝

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) = def_ X xs
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  simp only [List.map_eq_self_iff]
  simp
  intro x _ a2 a3
  subst a2
  contradiction
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) = eq_ x y
Tactic:
case eq_ x y =>
  simp
  constructor
  case left | right =>
    intro a1 a2
    subst a1
    contradiction
State after:
no goals

State before:
v t : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  tauto
State after:
no goals

State before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).iff_ (replaceFreeAux v t binders psi) = phi.iff_ psi
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp
  tauto
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  apply phi_ih
  simp
  left
  exact h1
State after:
no goals

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = def_ a✝¹ a✝
Tactic:
simp only [replaceFreeAux]
State after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = def_ a✝¹ a✝

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) = def_ X xs
Tactic:
simp
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs = xs

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs = xs
Tactic:
simp only [List.map_eq_self_iff]
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, (if v = x ∧ x ∉ binders then t else x) = x

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, (if v = x ∧ x ∉ binders then t else x) = x
Tactic:
simp
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, v = x → x ∉ binders → t = x

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, v = x → x ∉ binders → t = x
Tactic:
intro x _ a2 a3
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
x : VarName
a✝ : x ∈ xs
a2 : v = x
a3 : x ∉ binders
⊢ t = x

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
x : VarName
a✝ : x ∈ xs
a2 : v = x
a3 : x ∉ binders
⊢ t = x
Tactic:
subst a2
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
a✝ : v ∈ xs
a3 : v ∉ binders
⊢ t = v

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
a✝ : v ∈ xs
a3 : v ∉ binders
⊢ t = v
Tactic:
contradiction
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) = eq_ x y
Tactic:
simp
State after:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ (v = x → x ∉ binders → t = x) ∧ (v = y → y ∉ binders → t = y)

State before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ (v = x → x ∉ binders → t = x) ∧ (v = y → y ∉ binders → t = y)
Tactic:
constructor
State after:
case left
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = x → x ∉ binders → t = x

case right
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y

State before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y
Tactic:
case left | right =>
  intro a1 a2
  subst a1
  contradiction
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y
Tactic:
intro a1 a2
State after:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
a1 : v = y
a2 : y ∉ binders
⊢ t = y

State before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
a1 : v = y
a2 : y ∉ binders
⊢ t = y
Tactic:
subst a1
State after:
v t x : VarName
binders : Finset VarName
h1 : v ∈ binders
a2 : v ∉ binders
⊢ t = v

State before:
v t x : VarName
binders : Finset VarName
h1 : v ∈ binders
a2 : v ∉ binders
⊢ t = v
Tactic:
contradiction
State after:
no goals

State before:
v t : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).not_ = phi.not_
Tactic:
tauto
State after:
no goals

State before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).iff_ (replaceFreeAux v t binders psi) = phi.iff_ psi
Tactic:
simp
State after:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders phi = phi ∧ replaceFreeAux v t binders psi = psi

State before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders phi = phi ∧ replaceFreeAux v t binders psi = psi
Tactic:
tauto
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) = exists_ x phi
Tactic:
simp
State after:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t (binders ∪ {x}) phi = phi

State before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t (binders ∪ {x}) phi = phi
Tactic:
apply phi_ih
State after:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∪ {x}

State before:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∪ {x}
Tactic:
simp
State after:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∨ v = x

State before:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∨ v = x
Tactic:
left
State after:
case h1.h
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders

State before:
case h1.h
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders
Tactic:
exact h1
State after:
no goals