Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case extra
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)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = 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)
Tactic:
suffices ∀ e, VExpr.instL ls e = VExpr.forallE A B →
    EnvStrong env df.uvars e df.type →
    (∃ u, IsDefEqStrong env U Γ A A (.sort u)) ∧
    (∃ u, IsDefEqStrong env U (A :: Γ) B B (.sort u)) by
  have ⟨A1, A2⟩ := envIH.2 h1
  cases eq <;> exact this _ ‹_› ‹_›
Proof state after:
case extra
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)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
⊢ ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)