Theorem: Lean4Lean.VEnv.IsDefEqStrong.weakN
Proof state before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k)
    (liftN n (instL ls✝ df✝.type) k)
Tactic:
simp [
  hA1.instL.liftN_eq (Nat.zero_le _),
  hA2.instL.liftN_eq (Nat.zero_le _),
  hA3.instL.liftN_eq (Nat.zero_le _)] at ih4 ih5 ⊢
Proof state after:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
⊢ IsDefEqStrong env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)