Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case beta.inr.forallE
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝¹ : VExpr
u✝ : VLevel
B✝¹ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝¹ A✝¹ (sort u✝)
h2 : IsDefEqStrong env U (A✝¹ :: Γ✝) B✝¹ B✝¹ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝¹
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝¹ e'✝) (inst B✝¹ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝¹ = forallE A B ∨ A✝¹ = 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 (A✝¹ :: Γ✝) →
      B✝¹ = forallE A B ∨ B✝¹ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝¹ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝¹ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝¹ e'✝ = forallE A B ∨ inst B✝¹ e'✝ = 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 Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝¹ :: Γ✝) (forallE A B) (forallE A B) B✝¹
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝¹ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝¹ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝¹ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝¹ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
eq : inst (forallE A B) e'✝ = forallE A✝ B✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v)
Tactic:
cases eq
Proof state after:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = 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 (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = 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
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
⊢ (∃ u, IsDefEqStrong env U Γ✝ (inst A e'✝) (inst A e'✝) (sort u)) ∧
    ∃ v, IsDefEqStrong env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1)) (inst B e'✝ (0 + 1)) (sort v)