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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E F
h2 : ∀ X ∈ F.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ F)
Tactic:
induction F
State after:
case meta_var_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
h2 : ∀ X ∈ (meta_var_ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ a✝))

case pred_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
h2 : ∀ X ∈ (pred_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ a✝¹ a✝))

case eq_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
h2 : ∀ X ∈ (eq_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ a✝¹ a✝))

case true_
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ true_)

case not_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ :
  IsMetaVarOrAllDefInEnv E a✝ →
    (∀ X ∈ a✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝)
h1 : IsMetaVarOrAllDefInEnv E a✝.not_
h2 : ∀ X ∈ a✝.not_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ a✝.not_)

case imp_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ :
  IsMetaVarOrAllDefInEnv E a✝¹ →
    (∀ X ∈ a✝¹.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝¹)
a_ih✝ :
  IsMetaVarOrAllDefInEnv E a✝ →
    (∀ X ∈ a✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝)
h1 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
h2 : ∀ X ∈ (a✝¹.imp_ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (a✝¹.imp_ a✝))

case forall_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  IsMetaVarOrAllDefInEnv E a✝ →
    (∀ X ∈ a✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝)
h1 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
h2 : ∀ X ∈ (forall_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ a✝¹ a✝))

case def_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
h2 : ∀ X ∈ (def_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ a✝¹ a✝))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : ∀ X_1 ∈ (meta_var_ X).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
Tactic:
case meta_var_ X =>
  unfold Formula.metaVarSet at h2
  simp at h2
  unfold sub
  exact h2
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
Tactic:
case pred_ X xs =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ x y))
Tactic:
case eq_ x y =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ true_)
Tactic:
case true_ =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi.not_
h2 : ∀ X ∈ phi.not_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold Formula.metaVarSet at h2
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h1 h2
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold Formula.metaVarSet at h2
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h1 h2
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
Tactic:
case def_ X xs =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp
  exact h1
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : ∀ X_1 ∈ (meta_var_ X).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
Tactic:
unfold Formula.metaVarSet at h2
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : ∀ X_1 ∈ {X}, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : ∀ X_1 ∈ {X}, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
Tactic:
simp at h2
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (τ X)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
exact h2
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (pred_ X (List.map (↑σ) xs))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (pred_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ True

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ True
Tactic:
simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ x y))
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (eq_ (↑σ x) (↑σ y))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (eq_ (↑σ x) (↑σ y))
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ True

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ True
Tactic:
simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ true_)
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E true_

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E true_
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ True

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ True
Tactic:
simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi.not_
h2 : ∀ X ∈ phi.not_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h2 : ∀ X ∈ phi.not_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h2 : ∀ X ∈ phi.not_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)
Tactic:
unfold Formula.metaVarSet at h2
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi).not_

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi).not_
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
Tactic:
exact phi_ih h1 h2
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
h2 : ∀ X ∈ (phi.imp_ psi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ X ∈ (phi.imp_ psi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ X ∈ (phi.imp_ psi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
unfold Formula.metaVarSet at h2
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
simp at h2
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E ((sub σ τ phi).imp_ (sub σ τ psi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E ((sub σ τ phi).imp_ (sub σ τ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Tactic:
cases h1
State after:
case intro
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Tactic:
constructor
State after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)

case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ psi)

State before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
Tactic:
apply phi_ih h1_left
State after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)

State before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
intro X a1
State after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)

State before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
apply h2
State after:
case left.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet

State before:
case left.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Tactic:
left
State after:
case left.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet

State before:
case left.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet
Tactic:
exact a1
State after:
no goals

State before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Tactic:
apply psi_ih h1_right
State after:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)

State before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
intro X a1
State after:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)

State before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
apply h2
State after:
case right.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet

State before:
case right.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Tactic:
right
State after:
case right.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ psi.metaVarSet

State before:
case right.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ psi.metaVarSet
Tactic:
exact a1
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
unfold Formula.metaVarSet at h2
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
Tactic:
exact phi_ih h1 h2
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
Tactic:
unfold sub
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
Tactic:
simp
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Tactic:
exact h1
State after:
no goals