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₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
⊢ (match next ofv✝ v with
      | none =>
        some (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝), VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝))
      | some v => do
        let __discr ← find? Δ₁✝ v
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) A)) =
      some (e₁, A₁) →
    (match next ofv✝ v with
        | none =>
          some (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝), VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝))
        | some v => do
          let __discr ← find? Δ₂✝ v
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) A)) =
        some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) 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₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ some (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝), VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝)) =
      some (e₁, A₁) →
    some (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝), VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝)) =
        some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) 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₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (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.vlet type₁✝ value₁✝)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) A)) =
      some (e₁, A₁) →
    (do
          let __discr ← find? Δ₂✝ v✝
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) A)) =
        some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁