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
e : VExpr
eq : VExpr.instL ls e = forallE A B
IH : EnvStrong env df.uvars e df.type
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
Tactic:
cases e <;> cases eq
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 Γ
binderType✝ body✝ : VExpr
IH : EnvStrong env df.uvars (forallE binderType✝ body✝) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls binderType✝) (VExpr.instL ls binderType✝) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝) (VExpr.instL ls body✝) (sort u)