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

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