Theorem: Lean4Lean.VEnv.IsDefEqStrong.weakN
Proof state before:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (const c✝ ls✝) k) (liftN n (const c✝ ls'✝) k) (liftN n (instL ls✝ ci✝.type) k)
Tactic:
simp [(henv.closedC h1).instL.liftN_eq (Nat.zero_le _)] at ih3 ih4 ⊢
Proof state after:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (liftN n (sort u✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (liftN n (sort u✝) k)
⊢ IsDefEqStrong env U Γ' (liftN n (const c✝ ls✝) k) (liftN n (const c✝ ls'✝) k) (instL ls✝ ci✝.type)