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

State before:
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
hΔ : VLCtx.WF env (List.length Us) Δ
e : Expr
e' : VExpr
H : TrExpr env Us Δ e e'
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) e'
Tactic:
induction H with
| bvar h1 | fvar h1 => exact ⟨_, hΔ.find?_wf henv h1⟩
| sort h1 => exact ⟨_, .sort (.of_ofLevel h1)⟩
| const h1 h2 h3 =>
  simp [List.mapM_eq_some] at h2
  refine ⟨_, .const h1 (fun l hl => ?_) (h2.length_eq.symm.trans h3)⟩
  have ⟨_, _, h⟩ := h2.forall_exists_r _ hl; exact .of_ofLevel h
| app h1 h2 => exact ⟨_, h1.app h2⟩
| lam h1 _ _ _ ih2 =>
  have ⟨_, h1'⟩ := h1
  have ⟨_, h2'⟩ := ih2 ⟨hΔ, nofun, h1⟩
  refine ⟨_, h1'.lam h2'⟩
| forallE h1 h2 => have ⟨_, h1'⟩ := h1; have ⟨_, h2'⟩ := h2; exact ⟨_, .forallE h1' h2'⟩
| letE h1 _ _ _ _ _ ih3 => exact ih3 ⟨hΔ, nofun, h1⟩
| lit _ ih | mdata _ ih => exact ih hΔ
| proj _ h2 ih => exact h2.wf (ih hΔ)
State after:
no goals

State before:
case fvar
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e✝
Tactic:
exact ⟨_, hΔ.find?_wf henv h1⟩
State after:
no goals

State before:
case sort
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
h1 : VLevel.ofLevel Us u✝ = some u'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝)
Tactic:
exact ⟨_, .sort (.of_ofLevel h1)⟩
State after:
no goals

State before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝)
Tactic:
simp [List.mapM_eq_some] at h2
State after:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝)

State before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝)
Tactic:
refine ⟨_, .const h1 (fun l hl => ?_) (h2.length_eq.symm.trans h3)⟩
State after:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
⊢ VLevel.WF (List.length Us) l

State before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
⊢ VLevel.WF (List.length Us) l
Tactic:
have ⟨_, _, h⟩ := h2.forall_exists_r _ hl
State after:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
w✝ : Level
left✝ : w✝ ∈ us✝
h : VLevel.ofLevel Us w✝ = some l
⊢ VLevel.WF (List.length Us) l

State before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
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✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
w✝ : Level
left✝ : w✝ ∈ us✝
h : VLevel.ofLevel Us w✝ = some l
⊢ VLevel.WF (List.length Us) l
Tactic:
exact .of_ofLevel h
State after:
no goals

State before:
case app
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) f'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) a'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.app f'✝ a'✝)
Tactic:
exact ⟨_, h1.app h2⟩
State after:
no goals

State before:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Tactic:
have ⟨_, h1'⟩ := h1
State after:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)

State before:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Tactic:
have ⟨_, h2'⟩ := ih2 ⟨hΔ, nofun, h1⟩
State after:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VExpr
h2' : IsDefEq env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝ body'✝ w✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)

State before:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VExpr
h2' : IsDefEq env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝ body'✝ w✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Tactic:
refine ⟨_, h1'.lam h2'⟩
State after:
no goals

State before:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Tactic:
have ⟨_, h1'⟩ := h1
State after:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)

State before:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Tactic:
have ⟨_, h2'⟩ := h2
State after:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VLevel
h2' : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)

State before:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VLevel
h2' : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Tactic:
exact ⟨_, .forallE h1' h2'⟩
State after:
no goals

State before:
case letE
env : VEnv
Δ : VLCtx
henv : Ordered env
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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) val'✝
ih3 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) body'✝
Tactic:
exact ih3 ⟨hΔ, nofun, h1⟩
State after:
no goals

State before:
case mdata
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e'✝
Tactic:
exact ih hΔ
State after:
no goals

State before:
case proj
env : VEnv
Δ : VLCtx
henv : Ordered env
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.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e''✝
Tactic:
exact h2.wf (ih hΔ)
State after:
no goals