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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ F)
⊢ IsMetaVarOrAllDefInEnv E F
Tactic:
induction F
State after:
case meta_var_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ a✝))
⊢ IsMetaVarOrAllDefInEnv E (meta_var_ a✝)

case pred_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)

case eq_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)

case true_
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ IsMetaVarOrAllDefInEnv E true_

case not_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝) → IsMetaVarOrAllDefInEnv E a✝
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ a✝.not_)
⊢ IsMetaVarOrAllDefInEnv E a✝.not_

case imp_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝¹) → IsMetaVarOrAllDefInEnv E a✝¹
a_ih✝ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝) → IsMetaVarOrAllDefInEnv E a✝
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (a✝¹.imp_ a✝))
⊢ IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)

case forall_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝) → IsMetaVarOrAllDefInEnv E a✝
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)

case def_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (def_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
⊢ IsMetaVarOrAllDefInEnv E (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

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

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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ IsMetaVarOrAllDefInEnv E true_
Tactic:
case true_ =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

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

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

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

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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
⊢ True
Tactic:
simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
⊢ IsMetaVarOrAllDefInEnv E (pred_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
⊢ True

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
⊢ True
Tactic:
simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ x y))
⊢ IsMetaVarOrAllDefInEnv E (eq_ x y)
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ x y))
⊢ True

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ x y))
⊢ True
Tactic:
simp only
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ IsMetaVarOrAllDefInEnv E true_
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ True

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ True
Tactic:
simp only
State after:
no goals

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

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

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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
⊢ IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
Tactic:
unfold sub at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1 : IsMetaVarOrAllDefInEnv E ((sub σ τ phi).imp_ (sub σ τ psi))
⊢ IsMetaVarOrAllDefInEnv E (phi.imp_ psi)

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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
Tactic:
cases h1
State after:
case intro
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
left✝ : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
right✝ : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
Tactic:
constructor
State after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi

case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E psi

State before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi
Tactic:
exact phi_ih h1_left
State after:
no goals

State before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E psi
Tactic:
exact psi_ih h1_right
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Tactic:
unfold sub at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E phi

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Tactic:
unfold sub at h1
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)

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

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

State before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
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
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