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

State before:
env : VEnv
Δ₁ Δ₂ : VLCtx
henv : Ordered env
Us : List Name
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
e : Expr
e₁ e₂ : VExpr
H1 : TrExpr env Us Δ₁ e e₁
H2 : TrExpr env Us Δ₂ e e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ₁) e₁ e₂
Tactic:
induction H1 generalizing Δ₂ e₂ with
| bvar l1 => let .bvar r1 := H2; exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
| fvar l1 => let .fvar r1 := H2; exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
| sort l1 => let .sort r1 := H2; cases l1.symm.trans r1; exact ⟨_, .sort (.of_ofLevel l1)⟩
| const l1 l2 l3 =>
  let .const r1 r2 r3 := H2; cases l1.symm.trans r1; cases l2.symm.trans r2
  exact (TrExpr.const l1 l2 l3).wf henv hΔ.wf
| app l1 l2 _ _ ih3 ih4 =>
  let .app _ _ r3 r4 := H2
  exact ⟨_, .appDF
    (ih3 hΔ r3 |>.of_l henv hΔ.wf.toCtx l1)
    (ih4 hΔ r4 |>.of_l henv hΔ.wf.toCtx l2)⟩
| lam l1 _ _ ih2 ih3 =>
  let ⟨_, l1⟩ := l1; let .lam _ r2 r3 := H2
  have hA := ih2 hΔ r2 |>.of_l henv hΔ.wf.toCtx l1
  have ⟨_, hb⟩ := ih3 (hΔ.cons nofun <| .vlam hA) r3
  exact ⟨_, .lamDF hA hb⟩
| forallE l1 l2 _ _ ih3 ih4 =>
  let ⟨_, l1'⟩ := l1; let ⟨_, l2⟩ := l2; let .forallE _ _ r3 r4 := H2
  have hA := ih3 hΔ r3 |>.of_l henv hΔ.wf.toCtx l1'
  have hB := ih4 (hΔ.cons nofun <| .vlam hA) r4 |>.of_l (Γ := _::_) henv ⟨hΔ.wf.toCtx, l1⟩ l2
  exact ⟨_, .forallEDF hA hB⟩
| letE l1 _ _ _ ih2 ih3 ih4 =>
  have hΓ := hΔ.wf.toCtx
  let .letE _ r2 r3 r4 := H2
  have ⟨_, hb⟩ := l1.isType henv hΓ
  refine ih4 (hΔ.cons nofun ?_) r4
  exact .vlet (ih3 hΔ r3 |>.of_l henv hΓ l1) (ih2 hΔ r2 |>.of_l henv hΓ hb)
| lit _ ih1 => let .lit r1 := H2; exact ih1 hΔ r1
| mdata _ ih1 => let .mdata r1 := H2; exact ih1 hΔ r1
| proj _ l2 ih1 => let .proj r1 r2 := H2; exact l2.uniq r2 (ih1 hΔ r1)
State after:
no goals

State before:
case bvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝ : VExpr
Δ✝ : VLCtx
i✝ : Nat
l1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.bvar i✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
let .bvar r1 := H2
State after:
case bvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
i✝ : Nat
l1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.bvar i✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inl i✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂

State before:
case bvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
i✝ : Nat
l1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.bvar i✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inl i✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
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
l1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.fvar fv✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
let .fvar r1 := H2
State after:
case fvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
l1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.fvar fv✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inr fv✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂

State before:
case fvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
l1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.fvar fv✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inr fv✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
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
l1 : VLevel.ofLevel Us u✝ = some u'✝
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝) e₂
Tactic:
let .sort r1 := H2
State after:
case sort
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝¹ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝¹
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
u'✝ : VLevel
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝¹) (VExpr.sort u'✝)

State before:
case sort
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝¹ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝¹
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
u'✝ : VLevel
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝¹) (VExpr.sort u'✝)
Tactic:
cases l1.symm.trans r1
State after:
case sort.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝) (VExpr.sort u'✝)

State before:
case sort.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝) (VExpr.sort u'✝)
Tactic:
exact ⟨_, .sort (.of_ofLevel l1)⟩
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
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝) e₂
Tactic:
let .const r1 r2 r3 := 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
l1 : env.constants c✝ = some (some ci✝¹)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝¹.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
ci✝ : VConstant
us'✝ : List VLevel
r1 : env.constants c✝ = some (some ci✝)
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (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
l1 : env.constants c✝ = some (some ci✝¹)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝¹.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
ci✝ : VConstant
us'✝ : List VLevel
r1 : env.constants c✝ = some (some ci✝)
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)
Tactic:
cases l1.symm.trans r1
State after:
case const.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝¹ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
us'✝ : List VLevel
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)

State before:
case const.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝¹ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
us'✝ : List VLevel
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)
Tactic:
cases l2.symm.trans r2
State after:
case const.refl.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝) (VExpr.const c✝ us'✝)

State before:
case const.refl.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝) (VExpr.const c✝ us'✝)
Tactic:
exact (TrExpr.const l1 l2 l3).wf henv hΔ.wf
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
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₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.app f'✝ a'✝) e₂
Tactic:
let .app _ _ r3 r4 := H2
State after:
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'✝)

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)⟩
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
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
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₂

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
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'✝)

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
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'✝)

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
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'✝)

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⟩
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
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
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₂

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
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₂

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
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'✝)

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'
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'✝)

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
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'✝)

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✝¹)
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'✝)
Tactic:
exact ⟨_, .forallEDF hA hB⟩
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
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₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
have hΓ := hΔ.wf.toCtx
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))
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂

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))
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
let .letE _ r2 r3 r4 := H2
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₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂

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₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
have ⟨_, hb⟩ := l1.isType henv hΓ
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✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂

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
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'✝)

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✝)
⊢ VLocalDecl.IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) (VLocalDecl.vlet ty'✝¹ val'✝¹) (VLocalDecl.vlet ty'✝ val'✝)
Tactic:
exact .vlet (ih3 hΔ r3 |>.of_l henv hΓ l1) (ih2 hΔ r2 |>.of_l henv hΓ hb)
State after:
no goals

State before:
case lit
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.lit l✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
let .lit r1 := H2
State after:
case lit
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.lit l✝) e₂
r1 : TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂

State before:
case lit
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.lit l✝) e₂
r1 : TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
exact ih1 hΔ r1
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'✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.mdata d✝ e✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Tactic:
let .mdata r1 := H2
State after:
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'✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.mdata d✝ e✝) e₂
r1 : TrExpr env Us Δ₂ e✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂

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'✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.mdata d✝ e✝) e₂
r1 : TrExpr env Us Δ₂ e✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Tactic:
exact ih1 hΔ r1
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'✝
l2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.proj s✝ i✝ e✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e''✝ e₂
Tactic:
let .proj r1 r2 := H2
State after:
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'✝¹
l2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝¹ e''✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.proj s✝ i✝ e✝) e₂
e'✝ : VExpr
r1 : TrExpr env Us Δ₂ e✝ e'✝
r2 : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ e'✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e''✝ e₂

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'✝¹
l2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝¹ e''✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.proj s✝ i✝ e✝) e₂
e'✝ : VExpr
r1 : TrExpr env Us Δ₂ e✝ e'✝
r2 : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ e'✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e''✝ e₂
Tactic:
exact l2.uniq r2 (ih1 hΔ r1)
State after:
no goals