Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))
Tactic:
rw [C1.liftN_eq (Nat.zero_le _), C2.liftN_eq (by exact Nat.le_refl _)] at this
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))