Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isBoundIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).boundVarSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isBoundIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).boundVarSet

case eq_
v a✝¹ a✝ : VarName
⊢ isBoundIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).boundVarSet

case true_
v : VarName
⊢ isBoundIn v true_ ↔ v ∈ true_.boundVarSet

case false_
v : VarName
⊢ isBoundIn v false_ ↔ v ∈ false_.boundVarSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝.not_ ↔ v ∈ a✝.not_.boundVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).boundVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).boundVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).boundVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).boundVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).boundVarSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).boundVarSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isBoundIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).boundVarSet
Tactic:
all_goals
  simp only [isBoundIn]
  simp only [Formula.boundVarSet]
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ False ↔ v ∈ ∅

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ False ↔ v ∈ ∅

case eq_
v a✝¹ a✝ : VarName
⊢ False ↔ v ∈ ∅

case true_
v : VarName
⊢ False ↔ v ∈ ∅

case false_
v : VarName
⊢ False ↔ v ∈ ∅

case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝¹ ∨ isBoundIn v a✝ ↔ v ∈ a✝¹.boundVarSet ∪ a✝.boundVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝¹ ∨ isBoundIn v a✝ ↔ v ∈ a✝¹.boundVarSet ∪ a✝.boundVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝¹ ∨ isBoundIn v a✝ ↔ v ∈ a✝¹.boundVarSet ∪ a✝.boundVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝¹ ∨ isBoundIn v a✝ ↔ v ∈ a✝¹.boundVarSet ∪ a✝.boundVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ v = a✝¹ ∨ isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet ∪ {a✝¹}

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ v = a✝¹ ∨ isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet ∪ {a✝¹}

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ v ∈ ∅