Theorem: FOL.NV.isFreeIn_imp_isFreeInInd (FOL/NV/Binders.lean)

State before:
v : VarName
F : Formula
h1 : isFreeIn v F
⊢ isFreeInInd v F
Tactic:
induction F
State after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_const_ a✝¹ a✝)
⊢ isFreeInInd v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_var_ a✝¹ a✝)
⊢ isFreeInInd v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : isFreeIn v (eq_ a✝¹ a✝)
⊢ isFreeInInd v (eq_ a✝¹ a✝)

case true_
v : VarName
h1 : isFreeIn v true_
⊢ isFreeInInd v true_

case false_
v : VarName
h1 : isFreeIn v false_
⊢ isFreeInInd v false_

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝.not_
⊢ isFreeInInd v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.imp_ a✝)
⊢ isFreeInInd v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.and_ a✝)
⊢ isFreeInInd v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.or_ a✝)
⊢ isFreeInInd v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.iff_ a✝)
⊢ isFreeInInd v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (forall_ a✝¹ a✝)
⊢ isFreeInInd v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (exists_ a✝¹ a✝)
⊢ isFreeInInd v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ isFreeInInd v (def_ a✝¹ a✝)

State before:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_const_ a✝¹ a✝)
⊢ isFreeInInd v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_var_ a✝¹ a✝)
⊢ isFreeInInd v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : isFreeIn v (eq_ a✝¹ a✝)
⊢ isFreeInInd v (eq_ a✝¹ a✝)

case true_
v : VarName
h1 : isFreeIn v true_
⊢ isFreeInInd v true_

case false_
v : VarName
h1 : isFreeIn v false_
⊢ isFreeInInd v false_

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝.not_
⊢ isFreeInInd v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.imp_ a✝)
⊢ isFreeInInd v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.and_ a✝)
⊢ isFreeInInd v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.or_ a✝)
⊢ isFreeInInd v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.iff_ a✝)
⊢ isFreeInInd v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (forall_ a✝¹ a✝)
⊢ isFreeInInd v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (exists_ a✝¹ a✝)
⊢ isFreeInInd v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ isFreeInInd v (def_ a✝¹ a✝)
Tactic:
any_goals
  simp only [isFreeIn] at h1
State after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : v ∈ a✝
⊢ isFreeInInd v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : v ∈ a✝
⊢ isFreeInInd v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : v = a✝¹ ∨ v = a✝
⊢ isFreeInInd v (eq_ a✝¹ a✝)

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝
⊢ isFreeInInd v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ isFreeInInd v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ isFreeInInd v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ isFreeInInd v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ isFreeInInd v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : ¬v = a✝¹ ∧ isFreeIn v a✝
⊢ isFreeInInd v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : ¬v = a✝¹ ∧ isFreeIn v a✝
⊢ isFreeInInd v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ isFreeInInd v (def_ a✝¹ a✝)

State before:
v : VarName
X : DefName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (def_ X xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y | def_ X xs =>
  first | exact isFreeInInd.pred_const_ X xs h1 | exact isFreeInInd.pred_var_ X xs h1 | exact isFreeInInd.eq_ x y h1 | exact isFreeInInd.def_ X xs h1
State after:
no goals

State before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi.not_
Tactic:
case not_ phi phi_ih =>
  apply isFreeInInd.not_
  exact phi_ih h1
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h1 : isFreeIn v phi ∨ isFreeIn v psi
⊢ isFreeInInd v (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 =>
  cases h1
  case inl c1 =>
    first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
    exact phi_ih c1
  case inr c1 =>
    first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
    exact psi_ih c1
State after:
no goals

State before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ isFreeInInd v (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
State after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ isFreeInInd v (def_ a✝¹ a✝)

State before:
v : VarName
X : DefName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (def_ X xs)
Tactic:
first | exact isFreeInInd.pred_const_ X xs h1 | exact isFreeInInd.pred_var_ X xs h1 | exact isFreeInInd.eq_ x y h1 | exact isFreeInInd.def_ X xs h1
State after:
no goals

State before:
v : VarName
X : PredName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (pred_const_ X xs)
Tactic:
exact isFreeInInd.pred_const_ X xs h1
State after:
no goals

State before:
v : VarName
X : PredName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (pred_var_ X xs)
Tactic:
exact isFreeInInd.pred_var_ X xs h1
State after:
no goals

State before:
v x y : VarName
h1 : v = x ∨ v = y
⊢ isFreeInInd v (eq_ x y)
Tactic:
exact isFreeInInd.eq_ x y h1
State after:
no goals

State before:
v : VarName
X : DefName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (def_ X xs)
Tactic:
exact isFreeInInd.def_ X xs h1
State after:
no goals

State before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi.not_
Tactic:
apply isFreeInInd.not_
State after:
case a
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
case a
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h1 : isFreeIn v phi ∨ isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
cases h1
State after:
case inl
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h✝ : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)

case inr
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h✝ : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
case inl c1 =>
  first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
  exact phi_ih c1
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
case inr c1 =>
  first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
  exact psi_ih c1
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Tactic:
exact phi_ih c1
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.imp_ psi)
Tactic:
apply isFreeInInd.imp_left_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.and_ psi)
Tactic:
apply isFreeInInd.and_left_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.or_ psi)
Tactic:
apply isFreeInInd.or_left_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
apply isFreeInInd.iff_left_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi

State before:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Tactic:
exact psi_ih c1
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.imp_ psi)
Tactic:
apply isFreeInInd.imp_right_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.and_ psi)
Tactic:
apply isFreeInInd.and_right_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.or_ psi)
Tactic:
apply isFreeInInd.or_right_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
apply isFreeInInd.iff_right_
State after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : ¬v = x ∧ isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Tactic:
cases h1
State after:
case intro
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
left✝ : ¬v = x
right✝ : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Tactic:
first | apply isFreeInInd.forall_ | apply isFreeInInd.exists_
State after:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (forall_ x phi)
Tactic:
apply isFreeInInd.forall_
State after:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Tactic:
apply isFreeInInd.exists_
State after:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi

State before:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x
Tactic:
exact h1_left
State after:
no goals

State before:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi
Tactic:
exact phi_ih h1_right
State after:
no goals