Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ : IsDefEq env U Δ₁ Δ₂
H1 : find? Δ₁ v = some (e₁, A₁)
H2 : find? Δ₂ v = some (e₂, A₂)
⊢ IsDefEqU env U (toCtx Δ₁) A₁ A₂ ∧ VEnv.IsDefEq env U (toCtx Δ₁) e₁ e₂ A₁
Tactic:
let .cons hΔ h1 h2 := hΔ
State after:
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₂✝
H1 : find? ((ofv✝, d₁✝) :: Δ₁✝) v = some (e₁, A₁)
H2 : find? ((ofv✝, d₂✝) :: Δ₂✝) v = some (e₂, A₂)
⊢ IsDefEqU env U (toCtx ((ofv✝, d₁✝) :: Δ₁✝)) A₁ A₂ ∧ VEnv.IsDefEq env U (toCtx ((ofv✝, d₁✝) :: Δ₁✝)) e₁ e₂ A₁

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✝)
H1 : find? ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝) v = some (e₁, A₁✝)
H2 : find? ((ofv✝, VLocalDecl.vlam A₂) :: Δ₂✝) v = 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:
revert H1 H2
State after:
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✝)
⊢ find? ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝) v = some (e₁, A₁✝) →
    find? ((ofv✝, VLocalDecl.vlam A₂) :: Δ₂✝) v = 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₁✝

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✝)
⊢ find? ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝) v = some (e₁, A₁✝) →
    find? ((ofv✝, VLocalDecl.vlam A₂) :: Δ₂✝) v = 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:
unfold VLCtx.find?
State after:
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₁✝

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
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₁✝

State before:
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₁✝
Tactic:
rintro ⟨⟩ ⟨⟩
State after:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.type (VLocalDecl.vlam A₁))
      (VLocalDecl.type (VLocalDecl.vlam A₂)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.value (VLocalDecl.vlam A₁))
      (VLocalDecl.value (VLocalDecl.vlam A₂)) (VLocalDecl.type (VLocalDecl.vlam A₁))

State before:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.type (VLocalDecl.vlam A₁))
      (VLocalDecl.type (VLocalDecl.vlam A₂)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.value (VLocalDecl.vlam A₁))
      (VLocalDecl.value (VLocalDecl.vlam A₂)) (VLocalDecl.type (VLocalDecl.vlam A₁))
Tactic:
exact ⟨⟨_, h2.weak henv⟩, .bvar .zero⟩
State after:
no goals

State before:
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₁✝
Tactic:
simp [bind, Option.bind_eq_some]
State after:
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✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.snd = A₁✝ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.snd = A₂✝ →
                  IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
                    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝

State before:
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✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.snd = A₁✝ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.snd = A₂✝ →
                  IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
                    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
rintro ⟨d₁', n₁'⟩ H1' rfl rfl ⟨d₂', n₂'⟩ H2' rfl rfl
State after:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)

State before:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
Tactic:
obtain ⟨h2, h3⟩ := find?_uniq hΔ H1' H2'
State after:
case h_2.mk.mk.intro
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
h2 : IsDefEqU env U (toCtx Δ₁✝) n₁' n₂'
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) d₁' d₂' n₁'
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)

State before:
case h_2.mk.mk.intro
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
h2 : IsDefEqU env U (toCtx Δ₁✝) n₁' n₂'
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) d₁' d₂' n₁'
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
Tactic:
exact ⟨h2.weakN henv .one, h3.weak henv⟩
State after:
no goals

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✝)
H1 : find? ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝) v = some (e₁, A₁)
H2 : find? ((ofv✝, VLocalDecl.vlet type₂✝ value₂✝) :: Δ₂✝) v = 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:
revert H1 H2
State after:
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✝)
⊢ find? ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝) v = some (e₁, A₁) →
    find? ((ofv✝, VLocalDecl.vlet type₂✝ value₂✝) :: Δ₂✝) v = 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₁

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✝)
⊢ find? ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝) v = some (e₁, A₁) →
    find? ((ofv✝, VLocalDecl.vlet type₂✝ value₂✝) :: Δ₂✝) v = 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:
unfold VLCtx.find?
State after:
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₁

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
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₁

State before:
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₁
Tactic:
rintro ⟨⟩ ⟨⟩
State after:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝))

State before:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝))
Tactic:
exact ⟨⟨_, h4⟩, h3⟩
State after:
no goals

State before:
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₁
Tactic:
simp [bind, Option.bind_eq_some]
State after:
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✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.snd = A₁ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.snd = 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₁

State before:
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✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.snd = A₁ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.snd = 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:
rintro ⟨d₁', n₁'⟩ H1' rfl rfl ⟨d₂', n₂'⟩ H2' rfl rfl
State after:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)

State before:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
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✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
Tactic:
simpa [VLocalDecl.depth] using find?_uniq hΔ H1' H2'
State after:
no goals