Theorem: Lean4Lean.TrExpr.weakN (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Us : List Name
e : Expr
e' : VExpr
W : VLCtx.LiftN Δ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
H : TrExpr env Us Δ e e'
⊢ TrExpr env Us Δ' e (VExpr.liftN n e' k)
Tactic:
induction H generalizing Δ' dk k with
| bvar h1 => exact .bvar (W.find? hΔ' h1)
| fvar h1 => exact .fvar (W.find? hΔ' h1)
| sort h1 => exact .sort h1
| const h1 h2 h3 => exact .const h1 h2 h3
| app h1 h2 _ _ ih1 ih2 =>
  exact .app (h1.weakN henv W.toCtx) (h2.weakN henv W.toCtx) (ih1 W hΔ') (ih2 W hΔ')
| lam h1 _ _ ih1 ih2 =>
  have h1 := h1.weakN henv W.toCtx
  exact .lam h1 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
| forallE h1 h2 _ _ ih1 ih2 =>
  have h1 := h1.weakN henv W.toCtx
  have h2 := h2.weakN henv W.toCtx.succ
  exact .forallE h1 h2 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
| letE h1 _ _ _ ih1 ih2 ih3 =>
  have h1 := h1.weakN henv W.toCtx
  exact .letE h1 (ih1 W hΔ') (ih2 W hΔ') (ih3 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
| lit _ ih => exact .lit (ih W hΔ')
| mdata _ ih => exact .mdata (ih W hΔ')
| proj _ h2 ih => exact .proj (ih W hΔ') (h2.weakN W.toCtx)
State after:
no goals

State before:
case bvar
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
i✝ : Nat
h1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.bvar i✝) (VExpr.liftN n e✝ k)
Tactic:
exact .bvar (W.find? hΔ' h1)
State after:
no goals

State before:
case fvar
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.fvar fv✝) (VExpr.liftN n e✝ k)
Tactic:
exact .fvar (W.find? hΔ' h1)
State after:
no goals

State before:
case sort
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
h1 : VLevel.ofLevel Us u✝ = some u'✝
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.sort u✝) (VExpr.liftN n (VExpr.sort u'✝) k)
Tactic:
exact .sort h1
State after:
no goals

State before:
case const
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
h3 : List.length us✝ = ci✝.uvars
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.const c✝ us✝) (VExpr.liftN n (VExpr.const c✝ us'✝) k)
Tactic:
exact .const h1 h2 h3
State after:
no goals

State before:
case app
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝² : Expr
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
a✝¹ : TrExpr env Us Δ✝ f✝ f'✝
a✝ : TrExpr env Us Δ✝ a✝² a'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' f✝ (VExpr.liftN n f'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' a✝² (VExpr.liftN n a'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.app f✝ a✝²) (VExpr.liftN n (VExpr.app f'✝ a'✝) k)
Tactic:
exact .app (h1.weakN henv W.toCtx) (h2.weakN henv W.toCtx) (ih1 W hΔ') (ih2 W hΔ')
State after:
no goals

State before:
case lam
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.lam name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.lam ty'✝ body'✝) k)
Tactic:
have h1 := h1.weakN henv W.toCtx
State after:
case lam
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.lam name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.lam ty'✝ body'✝) k)

State before:
case lam
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.lam name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.lam ty'✝ body'✝) k)
Tactic:
exact .lam h1 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
State after:
no goals

State before:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Tactic:
have h1 := h1.weakN henv W.toCtx
State after:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)

State before:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Tactic:
have h2 := h2.weakN henv W.toCtx.succ
State after:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
h2 : IsType env (List.length Us) (VExpr.liftN n ty'✝ k :: VLCtx.toCtx Δ') (VExpr.liftN n body'✝ (k + 1))
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)

State before:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
h2 : IsType env (List.length Us) (VExpr.liftN n ty'✝ k :: VLCtx.toCtx Δ') (VExpr.liftN n body'✝ (k + 1))
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Tactic:
exact .forallE h1 h2 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
State after:
no goals

State before:
case letE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' val✝ (VExpr.liftN n val'✝ k)
ih3 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VExpr.liftN n body'✝ k)
Tactic:
have h1 := h1.weakN henv W.toCtx
State after:
case letE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' val✝ (VExpr.liftN n val'✝ k)
ih3 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n val'✝ k) (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VExpr.liftN n body'✝ k)

State before:
case letE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' val✝ (VExpr.liftN n val'✝ k)
ih3 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n val'✝ k) (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VExpr.liftN n body'✝ k)
Tactic:
exact .letE h1 (ih1 W hΔ') (ih2 W hΔ') (ih3 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
State after:
no goals

State before:
case lit
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' (Literal.toConstructor l✝) (VExpr.liftN n e✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.lit l✝) (VExpr.liftN n e✝ k)
Tactic:
exact .lit (ih W hΔ')
State after:
no goals

State before:
case mdata
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' e✝ (VExpr.liftN n e'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.mdata d✝ e✝) (VExpr.liftN n e'✝ k)
Tactic:
exact .mdata (ih W hΔ')
State after:
no goals

State before:
case proj
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
a✝ : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' e✝ (VExpr.liftN n e'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.proj s✝ i✝ e✝) (VExpr.liftN n e''✝ k)
Tactic:
exact .proj (ih W hΔ') (h2.weakN W.toCtx)
State after:
no goals