Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case beta
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
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst B✝ e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e'✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst B✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k) (inst (sort v✝) e₀ k)
ih6 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst e✝ e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (app (lam A✝ e✝) e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
Tactic:
rw [inst0_inst_hi, inst0_inst_hi]
Proof state after:
case beta
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
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst B✝ e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e'✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst B✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k) (inst (sort v✝) e₀ k)
ih6 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst e✝ e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (app (lam A✝ e✝) e'✝) e₀ k) (inst (inst e✝ e₀ (k + 1)) (inst e'✝ e₀ k))
    (inst (inst B✝ e₀ (k + 1)) (inst e'✝ e₀ k))