Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case constDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (VExpr.sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (VExpr.sort u✝)
a_ih✝³ :
  VExpr.instL ls✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls✝ ci✝.type = 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✝² :
  VExpr.instL ls'✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls'✝ ci✝.type = 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✝¹ :
  VExpr.instL ls✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls✝ ci✝.type = 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✝ :
  VExpr.instL ls'✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls'✝ ci✝.type = 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 : VExpr.const c✝ ls✝ = VExpr.const c ls ∨ VExpr.const c✝ ls'✝ = 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
Proof state after:
case constDF.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
ci✝ : VConstant
ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (VExpr.sort u✝)
a✝² : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (VExpr.sort u✝)
a_ih✝³ a_ih✝² :
  VExpr.instL ls'✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls'✝ ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
h1 : env.constants c = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
h4 : List.length ls = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'✝
a✝¹ : IsDefEqStrong env U [] (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a_ih✝¹ a_ih✝ :
  VExpr.instL ls ci✝.type = VExpr.const c ls ∨ VExpr.instL ls ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars

case constDF.inr.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
ci✝ : VConstant
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (VExpr.sort u✝)
a✝² : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (VExpr.sort u✝)
a_ih✝³ a_ih✝² :
  VExpr.instL ls✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls✝ ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
h1 : env.constants c = some (some ci✝)
h3 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls
a✝¹ : IsDefEqStrong env U [] (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a_ih✝¹ a_ih✝ :
  VExpr.instL ls ci✝.type = VExpr.const c ls ∨ VExpr.instL ls ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars