Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
l2✝ : 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'✝¹
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝)) body'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.forallE name✝ ty✝ body✝ bi✝) e₂
w✝¹ : VLevel
l1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝¹)
w✝ : VLevel
l2 : HasType env (List.length Us) (ty'✝¹ :: VLCtx.toCtx Δ✝) body'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝¹ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
a✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ₂) body'✝
r3 : TrExpr env Us Δ₂ ty✝ ty'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
hA : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ ty'✝ (VExpr.sort w✝¹)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝¹ body'✝¹) (VExpr.forallE ty'✝ body'✝)
Tactic:
have hB := ih4 (hΔ.cons nofun <| .vlam hA) r4 |>.of_l (Γ := _::_) henv ⟨hΔ.wf.toCtx, l1⟩ l2
Proof 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
l1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
l2✝ : 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'✝¹
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝)) body'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.forallE name✝ ty✝ body✝ bi✝) e₂
w✝¹ : VLevel
l1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝¹)
w✝ : VLevel
l2 : HasType env (List.length Us) (ty'✝¹ :: VLCtx.toCtx Δ✝) body'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝¹ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
a✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ₂) body'✝
r3 : TrExpr env Us Δ₂ ty✝ ty'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
hA : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ ty'✝ (VExpr.sort w✝¹)
hB : IsDefEq env (List.length Us) (ty'✝¹ :: VLCtx.toCtx Δ✝) body'✝¹ body'✝ (VExpr.sort w✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝¹ body'✝¹) (VExpr.forallE ty'✝ body'✝)