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 Γ✝ Γ'
⊢ 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:
have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
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)
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)