Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
⊢ (match next ofv✝ v with
      | none => some (VLocalDecl.value (VLocalDecl.vlam A₁), VLocalDecl.type (VLocalDecl.vlam A₁))
      | some v => do
        let __discr ← find? Δ₁✝ v
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) A)) =
      some (e₁, A₁✝) →
    (match next ofv✝ v with
        | none => some (VLocalDecl.value (VLocalDecl.vlam A₂), VLocalDecl.type (VLocalDecl.vlam A₂))
        | some v => do
          let __discr ← find? Δ₂✝ v
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) A)) =
        some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
split
Proof state after:
case h_1
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ some (VLocalDecl.value (VLocalDecl.vlam A₁), VLocalDecl.type (VLocalDecl.vlam A₁)) = some (e₁, A₁✝) →
    some (VLocalDecl.value (VLocalDecl.vlam A₂), VLocalDecl.type (VLocalDecl.vlam A₂)) = some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝

case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ (do
        let __discr ← find? Δ₁✝ v✝
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) A)) =
      some (e₁, A₁✝) →
    (do
          let __discr ← find? Δ₂✝ v✝
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) A)) =
        some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝