Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = 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 : h✝ = forallE A B ∨ h'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
obtain eq | eq := eq
Proof state after:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = 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 : h✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)

case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = 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 : h'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)