Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case beta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ :
  A✝ = VExpr.const c ls ∨ A✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝³ :
  B✝ = VExpr.const c ls ∨ B✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝² :
  e✝ = VExpr.const c ls ∨ e✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝¹ :
  e'✝ = VExpr.const c ls ∨ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝ :
  inst B✝ e'✝ = VExpr.const c ls ∨ inst B✝ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ihee :
  inst e✝ e'✝ = VExpr.const c ls ∨ inst e✝ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : app (lam A✝ e✝) e'✝ = VExpr.const c ls ∨ inst e✝ e'✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case beta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ :
  A✝ = VExpr.const c ls ∨ A✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝³ :
  B✝ = VExpr.const c ls ∨ B✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝² :
  e✝ = VExpr.const c ls ∨ e✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝¹ :
  e'✝ = VExpr.const c ls ∨ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝ :
  inst B✝ e'✝ = VExpr.const c ls ∨ inst B✝ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ihee :
  inst e✝ e'✝ = VExpr.const c ls ∨ inst e✝ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : inst e✝ e'✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars