Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)
Tactic:
have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
Proof state after:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)