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

State before:
case refl
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ : VLCtx
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U Δ✝
H : VLCtx.find? Δ✝ v = some (e, A)
⊢ VLCtx.find? Δ✝ v = some (VExpr.liftN 0 e, VExpr.liftN 0 A)
Tactic:
simp [H]
State after:
no goals

State before:
case skip_fvar
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
H : VLCtx.find? Δ✝ v = some (e, A)
⊢ VLCtx.find? ((some fv', d✝) :: Δ') v =
    some (VExpr.liftN (n✝ + VLocalDecl.depth d✝) e, VExpr.liftN (n✝ + VLocalDecl.depth d✝) A)
Tactic:
simp [VLCtx.find?]
State after:
case skip_fvar
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
H : VLCtx.find? Δ✝ v = some (e, A)
⊢ (match next (some fv') v with
    | none => some (VLocalDecl.value d✝, VLocalDecl.type d✝)
    | some v =>
      Option.bind (VLCtx.find? Δ' v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d✝) __discr.fst, VExpr.liftN (VLocalDecl.depth d✝) __discr.snd)) =
    some (VExpr.liftN (n✝ + VLocalDecl.depth d✝) e, VExpr.liftN (n✝ + VLocalDecl.depth d✝) A)

State before:
case skip_fvar.inl
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
val✝ : Nat
H : VLCtx.find? Δ✝ (Sum.inl val✝) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ' (Sum.inl val✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth d✝) a.fst = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
        VExpr.liftN (VLocalDecl.depth d✝) a.snd = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
exact ⟨_, ih hΔ'.1 H, by simp [VExpr.liftN_liftN]⟩
State after:
no goals

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
val✝ : Nat
H : VLCtx.find? Δ✝ (Sum.inl val✝) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).fst =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).snd =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
simp [VExpr.liftN_liftN]
State after:
no goals

State before:
case skip_fvar.inr
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ (match if (fv' == fv) = true then none else some (Sum.inr fv) with
    | none => some (VLocalDecl.value d✝, VLocalDecl.type d✝)
    | some v =>
      Option.bind (VLCtx.find? Δ' v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d✝) __discr.fst, VExpr.liftN (VLocalDecl.depth d✝) __discr.snd)) =
    some (VExpr.liftN (n✝ + VLocalDecl.depth d✝) e, VExpr.liftN (n✝ + VLocalDecl.depth d✝) A)
Tactic:
cases eq : fv' == fv <;> simp
State after:
case skip_fvar.inr.false
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = false
⊢ ∃ a,
    VLCtx.find? Δ' (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth d✝) a.fst = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
        VExpr.liftN (VLocalDecl.depth d✝) a.snd = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A

case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ VLocalDecl.value d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VLocalDecl.type d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A

State before:
case skip_fvar.inr.false
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = false
⊢ ∃ a,
    VLCtx.find? Δ' (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth d✝) a.fst = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
        VExpr.liftN (VLocalDecl.depth d✝) a.snd = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
exact ⟨_, ih hΔ'.1 H, by simp [VExpr.liftN_liftN]⟩
State after:
no goals

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = false
⊢ VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).fst =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).snd =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
simp [VExpr.liftN_liftN]
State after:
no goals

State before:
case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ VLocalDecl.value d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VLocalDecl.type d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
refine ((List.pairwise_cons.1 hΔ'.fvars_nodup).1 fv' ?_ rfl).elim
State after:
case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ fv' ∈ List.filterMap (fun x => x.fst) Δ'

State before:
case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ fv' ∈ List.filterMap (fun x => x.fst) Δ'
Tactic:
exact W.fvars_suffix.subset ((beq_iff_eq ..).1 eq ▸ find?_eq_some.1 ⟨_, H⟩)
State after:
no goals

State before:
case cons_bvar
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H : VLCtx.find? ((none, d) :: Δ✝) v = some (e, A)
⊢ VLCtx.find? ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝) v =
    some (VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d), VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d))
Tactic:
simp [VLCtx.find?] at H ⊢
State after:
case cons_bvar
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H :
  (match next none v with
    | none => some (VLocalDecl.value d, VLocalDecl.type d)
    | some v =>
      Option.bind (VLCtx.find? Δ✝ v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd)) =
    some (e, A)
⊢ (match next none v with
    | none => some (VLocalDecl.value (VLocalDecl.liftN d n✝ k✝), VLocalDecl.type (VLocalDecl.liftN d n✝ k✝))
    | some v =>
      Option.bind (VLCtx.find? Δ'✝ v) fun __discr =>
        some
          (VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.fst,
            VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.snd)) =
    some (VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d), VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d))

State before:
case cons_bvar
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H :
  (match next none v with
    | none => some (VLocalDecl.value d, VLocalDecl.type d)
    | some v =>
      Option.bind (VLCtx.find? Δ✝ v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd)) =
    some (e, A)
⊢ (match next none v with
    | none => some (VLocalDecl.value (VLocalDecl.liftN d n✝ k✝), VLocalDecl.type (VLocalDecl.liftN d n✝ k✝))
    | some v =>
      Option.bind (VLCtx.find? Δ'✝ v) fun __discr =>
        some
          (VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.fst,
            VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.snd)) =
    some (VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d), VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d))
Tactic:
obtain ⟨_|i⟩ | fv := v <;> simp [VLCtx.next, bind] at H ⊢ <;>
  [(obtain ⟨rfl, rfl⟩ := H);
   (obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
    refine ⟨_, ih (v := .inl i) hΔ'.1 H, ?_⟩);
   (obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
    refine ⟨_, ih (v := .inr fv) hΔ'.1 H, ?_⟩)] <;>
  open VLocalDecl in
  cases d <;> simp [VExpr.lift_liftN', liftN, value, type, depth, VExpr.liftN]
State after:
no goals

State before:
case cons_bvar.inl.zero
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H : VLocalDecl.value d = e ∧ VLocalDecl.type d = A
⊢ VLocalDecl.value (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d) ∧
    VLocalDecl.type (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d)
Tactic:
obtain ⟨rfl, rfl⟩ := H
State after:
case cons_bvar.inl.zero.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
⊢ VLocalDecl.value (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ (VLocalDecl.value d) (k✝ + VLocalDecl.depth d) ∧
    VLocalDecl.type (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ (VLocalDecl.type d) (k✝ + VLocalDecl.depth d)

State before:
case cons_bvar.inl.succ
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
i : Nat
H :
  ∃ a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth d) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) a.snd = A
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst = VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd = VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d)
Tactic:
obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
State after:
case cons_bvar.inl.succ.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
i : Nat
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inl i) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)

State before:
case cons_bvar.inl.succ.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
i : Nat
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inl i) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Tactic:
refine ⟨_, ih (v := .inl i) hΔ'.1 H, ?_⟩
State after:
case cons_bvar.inl.succ.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
i : Nat
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inl i) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).fst =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
    VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).snd =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)

State before:
case cons_bvar.inr
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
H :
  ∃ a,
    VLCtx.find? Δ✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth d) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) a.snd = A
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst = VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd = VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d)
Tactic:
obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
State after:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)

State before:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Tactic:
refine ⟨_, ih (v := .inr fv) hΔ'.1 H, ?_⟩
State after:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).fst =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
    VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).snd =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)

State before:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).fst =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
    VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).snd =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Tactic:
cases d <;> simp [VExpr.lift_liftN', liftN, value, type, depth, VExpr.liftN]
State after:
no goals