Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
val'✝ ty'✝ : VExpr
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) val'✝ ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us Δ₂ val✝ val'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ₂) body✝ e₂
w✝ : VLevel
hb : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
refine ih4 (hΔ.cons nofun ?_) r4
Proof state after:
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
val'✝ ty'✝ : VExpr
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) val'✝ ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us Δ₂ val✝ val'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ₂) body✝ e₂
w✝ : VLevel
hb : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
⊢ VLocalDecl.IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) (VLocalDecl.vlet ty'✝¹ val'✝¹) (VLocalDecl.vlet ty'✝ val'✝)