Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN (Lean4Lean/Theory/Typing/Strong.lean)

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
k : Nat
Γ₁ Γ : List VExpr
e1 e2 A : VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ₁ Γ
H : IsDefEqStrong env U Γ₁ e1 e2 A
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst e1 e₀ k) (inst e2 e₀ k) (inst A e₀ k)
Tactic:
induction H generalizing Γ k with
| @bvar _ i ty _ h _ h2 ih =>
  dsimp [inst]; clear h2 ih
  induction W generalizing i ty with
  | zero =>
    cases h with simp [inst_lift]
    | zero => exact h₀
    | succ h =>
      let ⟨u, hty⟩ := hΓ₀.lookup henv h
      exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
  | succ _ ih =>
    cases h with (simp; rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)])
    | zero =>
      let ⟨u, hty⟩ := hΓ.lookup henv .zero
      exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
    | succ h => exact (ih h hΓ.1).weakN henv .one
| symm _ ih => exact .symm (ih W hΓ)
| trans _ _ ih1 ih2 => exact .trans (ih1 W hΓ) (ih2 W hΓ)
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| constDF h1 h2 h3 h4 h5 h6 h7 h8 _ _ _ _ ih3 ih4 =>
  simp [(henv.closedC h1).instL.instN_eq (Nat.zero_le _)] at ih3 ih4 ⊢
  exact .constDF h1 h2 h3 h4 h5 h6 h7 h8 (ih3 W hΓ) (ih4 W hΓ)
| appDF h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact inst0_inst_hi .. ▸ .appDF h1 h2
    (ih1 W hΓ) (ih2 W.succ ⟨hΓ, _, ih1 W hΓ⟩)
    (ih3 W hΓ) (ih4 W hΓ) (inst0_inst_hi .. ▸ inst0_inst_hi .. ▸ ih5 W hΓ)
| lamDF h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact
    have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
    have hΓ'' := ⟨hΓ, _, (ih1 W hΓ).hasType.2⟩
    .lamDF h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ') (ih3 W.succ hΓ'') (ih4 W.succ hΓ') (ih5 W.succ hΓ'')
| forallEDF h1 h2 _ _ _ ih1 ih2 ih3 =>
  exact .forallEDF h1 h2 (ih1 W hΓ)
    (ih2 W.succ ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩) (ih3 W.succ ⟨hΓ, _, (ih1 W hΓ).hasType.2⟩)
| defeqDF h1 _ _ ih1 ih2 => exact .defeqDF h1 (ih1 W hΓ) (ih2 W hΓ)
| beta h1 h2 _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 ih6 =>
  rw [inst0_inst_hi, inst0_inst_hi]; exact
    have hΓ' := ⟨hΓ, _, ih1 W hΓ⟩
    .beta h1 h2
      (ih1 W hΓ) (ih2 W.succ hΓ') (ih3 W.succ hΓ') (ih4 W hΓ)
      (inst0_inst_hi .. ▸ ih5 W hΓ) (inst0_inst_hi .. ▸ inst0_inst_hi .. ▸ ih6 W hΓ)
| eta h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  have :=
    have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
    IsDefEqStrong.eta h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ')
      (by
        have := ih3 W.succ.succ ⟨hΓ', _, by
          rw [← lift_instN_lo]; exact (ih1 W hΓ).hasType.1.weakN henv .one⟩
        rwa [lift_instN_lo, liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
      (ih4 W hΓ)
      (by
        have := ih5 W.succ hΓ'
        simp only [inst, ← lift_instN_lo] at this
        rwa [liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
  rw [lift, liftN_instN_lo (hj := Nat.zero_le _), Nat.add_comm] at this
  simpa [inst]
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel (ih1 W hΓ) (ih2 W hΓ) (ih3 W hΓ)
| extra h1 h2 h3 h4 h5 h6 h7 _ _ _ _ _ ih4 ih5 =>
  have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
  simp [
    hA1.instL.instN_eq (Nat.zero_le _),
    hA2.instL.instN_eq (Nat.zero_le _),
    hA3.instL.instN_eq (Nat.zero_le _)] at ih4 ih5 ⊢
  exact .extra h1 h2 h3 h4 h5 h6 h7 (ih4 W hΓ) (ih5 W hΓ)
State after:
no goals

State before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
h2 : IsDefEqStrong env U Γ✝ ty ty (sort u✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst ty e₀ k) (inst ty e₀ k) (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (VExpr.bvar i) e₀ k) (inst (VExpr.bvar i) e₀ k) (inst ty e₀ k)
Tactic:
dsimp [inst]
State after:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
h2 : IsDefEqStrong env U Γ✝ ty ty (sort u✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst ty e₀ k) (inst ty e₀ k) (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)

State before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
h2 : IsDefEqStrong env U Γ✝ ty ty (sort u✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst ty e₀ k) (inst ty e₀ k) (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Tactic:
clear h2 ih
State after:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)

State before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Tactic:
induction W generalizing i ty with
| zero =>
  cases h with simp [inst_lift]
  | zero => exact h₀
  | succ h =>
    let ⟨u, hty⟩ := hΓ₀.lookup henv h
    exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
| succ _ ih =>
  cases h with (simp; rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)])
  | zero =>
    let ⟨u, hty⟩ := hΓ.lookup henv .zero
    exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
  | succ h => exact (ih h hΓ.1).weakN henv .one
State after:
no goals

State before:
case bvar.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
i : Nat
ty : VExpr
h : Lookup (A₀ :: Γ₀) i ty
hΓ : CtxStrong env U Γ₀
⊢ IsDefEqStrong env U Γ₀ (instVar i e₀) (instVar i e₀) (inst ty e₀)
Tactic:
cases h with simp [inst_lift]
| zero => exact h₀
| succ h =>
  let ⟨u, hty⟩ := hΓ₀.lookup henv h
  exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
State after:
no goals

State before:
case bvar.zero.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
⊢ IsDefEqStrong env U Γ₀ e₀ e₀ A₀
Tactic:
exact h₀
State after:
no goals

State before:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
⊢ IsDefEqStrong env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝
Tactic:
let ⟨u, hty⟩ := hΓ₀.lookup henv h
State after:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
u : VLevel
hty : IsDefEqStrong env U Γ₀ ty✝ ty✝ (sort u)
⊢ IsDefEqStrong env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝

State before:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
u : VLevel
hty : IsDefEqStrong env U Γ₀ ty✝ ty✝ (sort u)
⊢ IsDefEqStrong env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝
Tactic:
exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
State after:
no goals

State before:
case bvar.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
i : Nat
ty : VExpr
h : Lookup (A✝ :: Γ✝) i ty
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (instVar i e₀ (k✝ + 1)) (instVar i e₀ (k✝ + 1)) (inst ty e₀ (k✝ + 1))
Tactic:
cases h with (simp; rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)])
| zero =>
  let ⟨u, hty⟩ := hΓ.lookup henv .zero
  exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
| succ h => exact (ih h hΓ.1).weakN henv .one
State after:
no goals

State before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (instVar (n✝ + 1) e₀ (k✝ + 1)) (instVar (n✝ + 1) e₀ (k✝ + 1))
    (inst (lift ty✝) e₀ (k✝ + 1))
Tactic:
simp
State after:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝))
    (inst (lift ty✝) e₀ (k✝ + 1))

State before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝))
    (inst (lift ty✝) e₀ (k✝ + 1))
Tactic:
rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)]
State after:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝))
    (liftN 1 (inst ty✝ e₀ k✝))

State before:
case bvar.succ.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (VExpr.bvar 0) (VExpr.bvar 0) (liftN 1 (inst A✝ e₀ k✝))
Tactic:
let ⟨u, hty⟩ := hΓ.lookup henv .zero
State after:
case bvar.succ.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
u : VLevel
hty : IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (inst A✝ e₀ k✝)) (lift (inst A✝ e₀ k✝)) (sort u)
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (VExpr.bvar 0) (VExpr.bvar 0) (liftN 1 (inst A✝ e₀ k✝))

State before:
case bvar.succ.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
u : VLevel
hty : IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (inst A✝ e₀ k✝)) (lift (inst A✝ e₀ k✝)) (sort u)
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (VExpr.bvar 0) (VExpr.bvar 0) (liftN 1 (inst A✝ e₀ k✝))
Tactic:
exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
State after:
no goals

State before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝))
    (liftN 1 (inst ty✝ e₀ k✝))
Tactic:
exact (ih h hΓ.1).weakN henv .one
State after:
no goals

State before:
case symm
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst e'✝ e₀ k) (inst e✝ e₀ k) (inst A✝ e₀ k)
Tactic:
exact .symm (ih W hΓ)
State after:
no goals

State before:
case trans
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEqStrong env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEqStrong env U Γ✝ e₂✝ e₃✝ A✝
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e₁✝ e₀ k) (inst e₂✝ e₀ k) (inst A✝ e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e₂✝ e₀ k) (inst e₃✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst e₁✝ e₀ k) (inst e₃✝ e₀ k) (inst A✝ e₀ k)
Tactic:
exact .trans (ih1 W hΓ) (ih2 W hΓ)
State after:
no goals

State before:
case sortDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
h2 : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (sort l✝) e₀ k) (inst (sort l'✝) e₀ k) (inst (sort (VLevel.succ l✝)) e₀ k)
Tactic:
exact .sortDF h1 h2 h3
State after:
no goals

State before:
case constDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
h6 : VLevel.WF U u✝
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (const c✝ ls✝) e₀ k) (inst (const c✝ ls'✝) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
Tactic:
simp [(henv.closedC h1).instL.instN_eq (Nat.zero_le _)] at ih3 ih4 ⊢
State after:
case constDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
h6 : VLevel.WF U u✝
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (inst (sort u✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (inst (sort u✝) e₀ k)
⊢ IsDefEqStrong env U Γ (inst (const c✝ ls✝) e₀ k) (inst (const c✝ ls'✝) e₀ k) (VExpr.instL ls✝ ci✝.type)

State before:
case constDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
h6 : VLevel.WF U u✝
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ ci✝.type) e₀ k) (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls'✝ ci✝.type) e₀ k) (inst (VExpr.instL ls'✝ ci✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (inst (sort u✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (inst (sort u✝) e₀ k)
⊢ IsDefEqStrong env U Γ (inst (const c✝ ls✝) e₀ k) (inst (const c✝ ls'✝) e₀ k) (VExpr.instL ls✝ ci✝.type)
Tactic:
exact .constDF h1 h2 h3 h4 h5 h6 h7 h8 (ih3 W hΓ) (ih4 W hΓ)
State after:
no goals

State before:
case appDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁵ a'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁵ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁵) (inst B✝ a'✝) (sort v✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst f✝ e₀ k) (inst f'✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst a✝⁵ e₀ k) (inst a'✝ e₀ k) (inst A✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst B✝ a✝⁵) e₀ k) (inst (inst B✝ a'✝) e₀ k) (inst (sort v✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (app f✝ a✝⁵) e₀ k) (inst (app f'✝ a'✝) e₀ k) (inst (inst B✝ a✝⁵) e₀ k)
Tactic:
exact inst0_inst_hi .. ▸ .appDF h1 h2
  (ih1 W hΓ) (ih2 W.succ ⟨hΓ, _, ih1 W hΓ⟩)
  (ih3 W hΓ) (ih4 W hΓ) (inst0_inst_hi .. ▸ inst0_inst_hi .. ▸ ih5 W hΓ)
State after:
no goals

State before:
case lamDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A'✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A'✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst body✝ e₀ k) (inst body'✝ e₀ k) (inst B✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A'✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst body✝ e₀ k) (inst body'✝ e₀ k) (inst B✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (lam A✝ body✝) e₀ k) (inst (lam A'✝ body'✝) e₀ k) (inst (forallE A✝ B✝) e₀ k)
Tactic:
exact
  have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
  have hΓ'' := ⟨hΓ, _, (ih1 W hΓ).hasType.2⟩
  .lamDF h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ') (ih3 W.succ hΓ'') (ih4 W.succ hΓ') (ih5 W.succ hΓ'')
State after:
no goals

State before:
case forallEDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A'✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst body✝ e₀ k) (inst body'✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A'✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst body✝ e₀ k) (inst body'✝ e₀ k) (inst (sort v✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (forallE A✝ body✝) e₀ k) (inst (forallE A'✝ body'✝) e₀ k)
    (inst (sort (VLevel.imax u✝ v✝)) e₀ k)
Tactic:
exact .forallEDF h1 h2 (ih1 W hΓ)
  (ih2 W.succ ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩) (ih3 W.succ ⟨hΓ, _, (ih1 W hΓ).hasType.2⟩)
State after:
no goals

State before:
case defeqDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
h1 : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst B✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e1✝ e₀ k) (inst e2✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst e1✝ e₀ k) (inst e2✝ e₀ k) (inst B✝ e₀ k)
Tactic:
exact .defeqDF h1 (ih1 W hΓ) (ih2 W hΓ)
State after:
no goals

State before:
case beta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst B✝ e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e'✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst B✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k) (inst (sort v✝) e₀ k)
ih6 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst e✝ e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (app (lam A✝ e✝) e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
Tactic:
rw [inst0_inst_hi, inst0_inst_hi]
State after:
case beta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst B✝ e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e'✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst B✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k) (inst (sort v✝) e₀ k)
ih6 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst e✝ e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (app (lam A✝ e✝) e'✝) e₀ k) (inst (inst e✝ e₀ (k + 1)) (inst e'✝ e₀ k))
    (inst (inst B✝ e₀ (k + 1)) (inst e'✝ e₀ k))

State before:
case beta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst B✝ e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e'✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst B✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k) (inst (sort v✝) e₀ k)
ih6 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (inst e✝ e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (app (lam A✝ e✝) e'✝) e₀ k) (inst (inst e✝ e₀ (k + 1)) (inst e'✝ e₀ k))
    (inst (inst B✝ e₀ (k + 1)) (inst e'✝ e₀ k))
Tactic:
exact
have hΓ' := ⟨hΓ, _, ih1 W hΓ⟩
.beta h1 h2
(ih1 W hΓ) (ih2 W.succ hΓ') (ih3 W.succ hΓ') (ih4 W hΓ)
(inst0_inst_hi .. ▸ ih5 W hΓ) (inst0_inst_hi .. ▸ inst0_inst_hi .. ▸ ih6 W hΓ)
State after:
no goals

State before:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
Tactic:
have :=
  have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
  IsDefEqStrong.eta h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ')
    (by
      have := ih3 W.succ.succ ⟨hΓ', _, by
        rw [← lift_instN_lo]; exact (ih1 W hΓ).hasType.1.weakN henv .one⟩
      rwa [lift_instN_lo, liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
    (ih4 W hΓ)
    (by
      have := ih5 W.succ hΓ'
      simp only [inst, ← lift_instN_lo] at this
      rwa [liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
State after:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
this :
  IsDefEqStrong env U Γ (lam (inst A✝ e₀ k) (app (lift (inst e✝ e₀ k)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)

State before:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
this :
  IsDefEqStrong env U Γ (lam (inst A✝ e₀ k) (app (lift (inst e✝ e₀ k)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
Tactic:
rw [lift, liftN_instN_lo (hj := Nat.zero_le _), Nat.add_comm] at this
State after:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
this :
  IsDefEqStrong env U Γ (lam (inst A✝ e₀ k) (app (inst (liftN 1 e✝) e₀ (k + 1)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)

State before:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
this :
  IsDefEqStrong env U Γ (lam (inst A✝ e₀ k) (app (inst (liftN 1 e✝) e₀ (k + 1)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
Tactic:
simpa [inst]
State after:
no goals

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ IsDefEqStrong env U (lift (inst A✝ e₀ k) :: inst A✝ e₀ k :: Γ) (liftN 1 (inst B✝ e₀ (k + 1)) 1)
    (liftN 1 (inst B✝ e₀ (k + 1)) 1) (sort v✝)
Tactic:
have := ih3 W.succ.succ ⟨hΓ', _, by
  rw [← lift_instN_lo]; exact (ih1 W hΓ).hasType.1.weakN henv .one⟩
State after:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst (lift A✝) e₀ (k + 1) :: inst A✝ e₀ k :: Γ) (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1))
    (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1)) (inst (sort v✝) e₀ (k + 1 + 1))
⊢ IsDefEqStrong env U (lift (inst A✝ e₀ k) :: inst A✝ e₀ k :: Γ) (liftN 1 (inst B✝ e₀ (k + 1)) 1)
    (liftN 1 (inst B✝ e₀ (k + 1)) 1) (sort v✝)

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst (lift A✝) e₀ (k + 1) :: inst A✝ e₀ k :: Γ) (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1))
    (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1)) (inst (sort v✝) e₀ (k + 1 + 1))
⊢ IsDefEqStrong env U (lift (inst A✝ e₀ k) :: inst A✝ e₀ k :: Γ) (liftN 1 (inst B✝ e₀ (k + 1)) 1)
    (liftN 1 (inst B✝ e₀ (k + 1)) 1) (sort v✝)
Tactic:
rwa [lift_instN_lo, liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1]
State after:
no goals

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (inst (lift A✝) e₀ (k + 1)) (inst (lift A✝) e₀ (k + 1)) (sort ?m.37173)
Tactic:
rw [← lift_instN_lo]
State after:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst A✝ e₀ k)) (lift (inst A✝ e₀ k)) (sort ?m.37173)

env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ VLevel

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst A✝ e₀ k)) (lift (inst A✝ e₀ k)) (sort ?m.37173)

env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ VLevel
Tactic:
exact (ih1 W hΓ).hasType.1.weakN henv .one
State after:
no goals

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))
Tactic:
have := ih5 W.succ hΓ'
State after:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (inst (lift e✝) e₀ (k + 1)) (inst (lift e✝) e₀ (k + 1))
    (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ (k + 1))
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (inst (lift e✝) e₀ (k + 1)) (inst (lift e✝) e₀ (k + 1))
    (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ (k + 1))
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))
Tactic:
simp only [inst, ← lift_instN_lo] at this
State after:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1)))
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))

State before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1)))
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))
Tactic:
rwa [liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1]
State after:
no goals

State before:
case proofIrrel
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
a✝¹ : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst p✝ e₀ k) (inst p✝ e₀ k) (inst (sort VLevel.zero) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst h✝ e₀ k) (inst h✝ e₀ k) (inst p✝ e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst h'✝ e₀ k) (inst h'✝ e₀ k) (inst p✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst h✝ e₀ k) (inst h'✝ e₀ k) (inst p✝ e₀ k)
Tactic:
exact .proofIrrel (ih1 W hΓ) (ih2 W hΓ) (ih3 W hΓ)
State after:
no goals

State before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)
Tactic:
have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
State after:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)

State before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)
Tactic:
simp [
  hA1.instL.instN_eq (Nat.zero_le _),
  hA2.instL.instN_eq (Nat.zero_le _),
  hA3.instL.instN_eq (Nat.zero_le _)] at ih4 ih5 ⊢
State after:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
⊢ IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)

State before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
⊢ IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3 h4 h5 h6 h7 (ih4 W hΓ) (ih5 W hΓ)
State after:
no goals