Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case constDF
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
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
h6 : VLevel.WF U u✝
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.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'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (const c✝ ls✝) e₀ k) (inst (const c✝ ls'✝) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
Tactic:
simp [(henv.closedC h1).instL.instN_eq (Nat.zero_le _)] at ih3 ih4 ⊢
Proof state after:
case constDF
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
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
h6 : VLevel.WF U u✝
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.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'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (inst (sort u✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (inst (sort u✝) e₀ k)
⊢ IsDefEqStrong env U Γ (inst (const c✝ ls✝) e₀ k) (inst (const c✝ ls'✝) e₀ k) (VExpr.instL ls✝ ci✝.type)