internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝¹ (VExpr.forallE A✝¹ B✝¹)
l2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝¹ A✝¹
a✝³ : TrExpr env Us Δ✝ f✝ f'✝¹
a✝² : TrExpr env Us Δ✝ a✝⁴ a'✝¹
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ f✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) f'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ a✝⁴ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) a'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.app f✝ a✝⁴) e₂
f'✝ A✝ B✝ a'✝ : VExpr
a✝¹ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) f'✝ (VExpr.forallE A✝ B✝)
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) a'✝ A✝
r3 : TrExpr env Us Δ₂ f✝ f'✝
r4 : TrExpr env Us Δ₂ a✝⁴ a'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.app f'✝¹ a'✝¹) (VExpr.app f'✝ a'✝)
Tactic:
exact ⟨_, .appDF
  (ih3 hΔ r3 |>.of_l henv hΔ.wf.toCtx l1)
  (ih4 hΔ r4 |>.of_l henv hΔ.wf.toCtx l2)⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝) e₂
Tactic:
let ⟨_, l1⟩ := l1
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝) e₂
Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝) e₂
Tactic:
let .lam _ r2 r3 := H2
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝¹
a✝¹ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝¹ body'✝¹) (VExpr.lam ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝¹
a✝¹ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝¹ body'✝¹) (VExpr.lam ty'✝ body'✝)
Tactic:
have hA := ih2 hΔ r2 |>.of_l henv hΔ.wf.toCtx l1
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝¹
a✝¹ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : 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.lam ty'✝¹ body'✝¹) (VExpr.lam ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝¹
a✝¹ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : 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.lam ty'✝¹ body'✝¹) (VExpr.lam ty'✝ body'✝)
Tactic:
have ⟨_, hb⟩ := ih3 (hΔ.cons nofun <| .vlam hA) r3
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝¹
a✝¹ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝¹ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝¹)
ty'✝ body'✝ : VExpr
a✝ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
hA : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ ty'✝ (VExpr.sort w✝¹)
w✝ : VExpr
hb : IsDefEq env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝)) body'✝¹ body'✝ w✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝¹ body'✝¹) (VExpr.lam ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof 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
l1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝¹
a✝¹ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) 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) ((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.lam name✝ ty✝ body✝ bi✝) e₂
w✝¹ : VLevel
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝¹)
ty'✝ body'✝ : VExpr
a✝ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
hA : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ ty'✝ (VExpr.sort w✝¹)
w✝ : VExpr
hb : IsDefEq env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝)) body'✝¹ body'✝ w✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝¹ body'✝¹) (VExpr.lam ty'✝ body'✝)
Tactic:
exact ⟨_, .lamDF hA hb⟩
Proof state after:
no goals
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₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝) e₂
Tactic:
let ⟨_, l1'⟩ := l1
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✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝) e₂
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✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝) e₂
Tactic:
let ⟨_, l2⟩ := 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✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝) e₂
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✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝) e₂
Tactic:
let .forallE _ _ r3 r4 := H2
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'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝¹ body'✝¹) (VExpr.forallE ty'✝ body'✝)
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'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝¹ body'✝¹) (VExpr.forallE ty'✝ body'✝)
Tactic:
have hA := ih3 hΔ r3 |>.of_l henv hΔ.wf.toCtx l1'
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✝¹)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝¹ body'✝¹) (VExpr.forallE ty'✝ body'✝)