Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free (FOL/MM0/MM0.lean)

State before:
F : Formula
vs : List VarName
v : VarName
Γ : List (VarName × MetaVarName)
h1 : NoMetaVarAndAllFreeInList vs F
h2 : v ∉ vs
⊢ NotFree Γ v F
Tactic:
induction F generalizing vs
State after:
case meta_var_
v : VarName
Γ : List (VarName × MetaVarName)
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ a✝)

case pred_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ a✝¹ a✝)

case eq_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (eq_ a✝¹ a✝)

case true_
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_

case not_
v : VarName
Γ : List (VarName × MetaVarName)
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
h2 : v ∉ vs
⊢ NotFree Γ v a✝.not_

case imp_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → v ∉ vs → NotFree Γ v a✝¹
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (a✝¹.imp_ a✝)

case forall_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (forall_ a✝¹ a✝)

case def_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ a✝¹ a✝)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ X xs)
Tactic:
case pred_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  tauto
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_
Tactic:
case true_ =>
  unfold NotFree
  simp
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : v ∉ vs
⊢ NotFree Γ v phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  exact phi_ih vs h1 h2
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ X xs)
Tactic:
case def_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  tauto
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ X)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h2 : v ∉ vs
h1 : False
⊢ NotFree Γ v (meta_var_ X)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h2 : v ∉ vs
h1 : False
⊢ NotFree Γ v (meta_var_ X)
Tactic:
contradiction
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (pred_ X xs)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (pred_ X xs)
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs
Tactic:
tauto
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
h2 : v ∉ vs
⊢ NotFree Γ v (eq_ x y)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ NotFree Γ v (eq_ x y)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ NotFree Γ v (eq_ x y)
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ ¬x = v ∧ ¬y = v

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ ¬x = v ∧ ¬y = v
Tactic:
cases h1
State after:
case intro
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
left✝ : x ∈ vs
right✝ : y ∈ vs
⊢ ¬x = v ∧ ¬y = v

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v ∧ ¬y = v
Tactic:
constructor
State after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v

case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬y = v

State before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v
Tactic:
intro contra
State after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ False

State before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ False
Tactic:
apply h2
State after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ v ∈ vs

State before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ v ∈ vs
Tactic:
subst contra
State after:
case left
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : x ∉ vs
⊢ x ∈ vs

State before:
case left
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : x ∉ vs
⊢ x ∈ vs
Tactic:
exact h1_left
State after:
no goals

State before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬y = v
Tactic:
intro contra
State after:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ False

State before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ False
Tactic:
apply h2
State after:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ v ∈ vs

State before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ v ∈ vs
Tactic:
subst contra
State after:
case right
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : y ∉ vs
⊢ y ∈ vs

State before:
case right
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : y ∉ vs
⊢ y ∈ vs
Tactic:
exact h1_right
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ True

State before:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ True
Tactic:
simp
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : v ∉ vs
⊢ NotFree Γ v phi.not_
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi.not_

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi.not_
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi
Tactic:
exact phi_ih vs h1 h2
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
h2 : v ∉ vs
⊢ NotFree Γ v (phi.imp_ psi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v (phi.imp_ psi)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v (phi.imp_ psi)
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
Tactic:
cases h1
State after:
case intro
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi

State before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
Tactic:
constructor
State after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi

case right
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v psi

State before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi
Tactic:
exact phi_ih vs h1_left h2
State after:
no goals

State before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v psi
Tactic:
exact psi_ih vs h1_right h2
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ x phi)
h2 : v ∉ vs
⊢ NotFree Γ v (forall_ x phi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NotFree Γ v (forall_ x phi)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NotFree Γ v (forall_ x phi)
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ x = v ∨ NotFree Γ v phi

State before:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ x = v ∨ NotFree Γ v phi
Tactic:
by_cases c1 : x = v
State after:
case pos
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v ∨ NotFree Γ v phi

case neg
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ x = v ∨ NotFree Γ v phi

State before:
case pos
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v ∨ NotFree Γ v phi
Tactic:
left
State after:
case pos.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v

State before:
case pos.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v
Tactic:
exact c1
State after:
no goals

State before:
case neg
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ x = v ∨ NotFree Γ v phi
Tactic:
right
State after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ NotFree Γ v phi

State before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ NotFree Γ v phi
Tactic:
apply phi_ih (x :: vs) h1
State after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ x :: vs

State before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ x :: vs
Tactic:
simp
State after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ ¬v = x ∧ v ∉ vs

State before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ ¬v = x ∧ v ∉ vs
Tactic:
push_neg
State after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x ∧ v ∉ vs

State before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x ∧ v ∉ vs
Tactic:
constructor
State after:
case neg.h.left
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x

case neg.h.right
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ vs

State before:
case neg.h.left
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x
Tactic:
tauto
State after:
no goals

State before:
case neg.h.right
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ vs
Tactic:
exact h2
State after:
no goals

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (def_ X xs)

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (def_ X xs)
Tactic:
unfold NotFree
State after:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs

State before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs
Tactic:
tauto
State after:
no goals