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

State before:
case bvar
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
u✝ : VLevel
h1 : Lookup Γ✝ i✝ A✝
h2 : VLevel.WF U u✝
h3 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A✝ k) (liftN n (sort u✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (VExpr.bvar i✝) k) (liftN n (VExpr.bvar i✝) k) (liftN n A✝ k)
Tactic:
refine .bvar (h1.weakN W) h2 (h3.weakN W)
State after:
no goals

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

State before:
case trans
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n e₁✝ k) (liftN n e₂✝ k) (liftN n A✝ k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n e₂✝ k) (liftN n e₃✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n e₁✝ k) (liftN n e₃✝ k) (liftN n A✝ k)
Tactic:
exact .trans (ih1 W) (ih2 W)
State after:
no goals

State before:
case sortDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (sort l✝) k) (liftN n (sort l'✝) k) (liftN n (sort (VLevel.succ l✝)) k)
Tactic:
exact .sortDF h1 h2 h3
State after:
no goals

State before:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (const c✝ ls✝) k) (liftN n (const c✝ ls'✝) k) (liftN n (instL ls✝ ci✝.type) k)
Tactic:
simp [(henv.closedC h1).instL.liftN_eq (Nat.zero_le _)] at ih3 ih4 ⊢
State after:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (liftN n (sort u✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (liftN n (sort u✝) k)
⊢ IsDefEqStrong env U Γ' (liftN n (const c✝ ls✝) k) (liftN n (const c✝ ls'✝) k) (instL ls✝ ci✝.type)

State before:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
h8 : IsDefEqStrong env U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ ci✝.type) k) (liftN n (instL ls✝ ci✝.type) k) (liftN n (sort u✝) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls'✝ ci✝.type) k) (liftN n (instL ls'✝ ci✝.type) k) (liftN n (sort u✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (liftN n (sort u✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (liftN n (sort u✝) k)
⊢ IsDefEqStrong env U Γ' (liftN n (const c✝ ls✝) k) (liftN n (const c✝ ls'✝) k) (instL ls✝ ci✝.type)
Tactic:
exact .constDF h1 h2 h3 h4 h5 h6 h7 h8 (ih3 W) (ih4 W)
State after:
no goals

State before:
case appDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n B✝ k) (liftN n B✝ k) (liftN n (sort v✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n f✝ k) (liftN n f'✝ k) (liftN n (forallE A✝ B✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n a✝⁵ k) (liftN n a'✝ k) (liftN n A✝ k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (inst B✝ a✝⁵) k) (liftN n (inst B✝ a'✝) k) (liftN n (sort v✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (app f✝ a✝⁵) k) (liftN n (app f'✝ a'✝) k) (liftN n (inst B✝ a✝⁵) k)
Tactic:
refine liftN_inst_hi .. ▸ .appDF h1 h2 (ih1 W) (ih2 W.succ) (ih3 W) (ih4 W) ?_
State after:
case appDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n B✝ k) (liftN n B✝ k) (liftN n (sort v✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n f✝ k) (liftN n f'✝ k) (liftN n (forallE A✝ B✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n a✝⁵ k) (liftN n a'✝ k) (liftN n A✝ k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (inst B✝ a✝⁵) k) (liftN n (inst B✝ a'✝) k) (liftN n (sort v✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (inst (liftN n B✝ (k + 1)) (liftN n a✝⁵ k)) (inst (liftN n B✝ (k + 1)) (liftN n a'✝ k))
    (sort v✝)

State before:
case appDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n B✝ k) (liftN n B✝ k) (liftN n (sort v✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n f✝ k) (liftN n f'✝ k) (liftN n (forallE A✝ B✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n a✝⁵ k) (liftN n a'✝ k) (liftN n A✝ k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (inst B✝ a✝⁵) k) (liftN n (inst B✝ a'✝) k) (liftN n (sort v✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (inst (liftN n B✝ (k + 1)) (liftN n a✝⁵ k)) (inst (liftN n B✝ (k + 1)) (liftN n a'✝ k))
    (sort v✝)
Tactic:
exact liftN_inst_hi .. ▸ liftN_inst_hi .. ▸ ih5 W
State after:
no goals

State before:
case lamDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A'✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n B✝ k) (liftN n B✝ k) (liftN n (sort v✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A'✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n B✝ k) (liftN n B✝ k) (liftN n (sort v✝) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n body✝ k) (liftN n body'✝ k) (liftN n B✝ k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A'✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n body✝ k) (liftN n body'✝ k) (liftN n B✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (lam A✝ body✝) k) (liftN n (lam A'✝ body'✝) k) (liftN n (forallE A✝ B✝) k)
Tactic:
exact .lamDF h1 h2 (ih1 W) (ih2 W.succ) (ih3 W.succ) (ih4 W.succ) (ih5 W.succ)
State after:
no goals

State before:
case forallEDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A'✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n body✝ k) (liftN n body'✝ k) (liftN n (sort v✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A'✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n body✝ k) (liftN n body'✝ k) (liftN n (sort v✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (forallE A✝ body✝) k) (liftN n (forallE A'✝ body'✝) k)
    (liftN n (sort (VLevel.imax u✝ v✝)) k)
Tactic:
exact .forallEDF h1 h2 (ih1 W) (ih2 W.succ) (ih3 W.succ)
State after:
no goals

State before:
case defeqDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n B✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n e1✝ k) (liftN n e2✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n e1✝ k) (liftN n e2✝ k) (liftN n B✝ k)
Tactic:
exact .defeqDF h1 (ih1 W) (ih2 W)
State after:
no goals

State before:
case beta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n A✝ k) (liftN n A✝ k) (liftN n (sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n B✝ k) (liftN n B✝ k) (liftN n (sort v✝) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEqStrong env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n B✝ k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n e'✝ k) (liftN n e'✝ k) (liftN n A✝ k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (inst B✝ e'✝) k) (liftN n (inst B✝ e'✝) k) (liftN n (sort v✝) k)
ih6 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (inst e✝ e'✝) k) (liftN n (inst e✝ e'✝) k) (liftN n (inst B✝ e'✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (app (lam A✝ e✝) e'✝) k) (liftN n (inst e✝ e'✝) k) (liftN n (inst B✝ e'✝) k)
Tactic:
refine liftN_inst_hi .. ▸ liftN_instN_hi .. ▸ .beta h1 h2
  (ih1 W) (ih2 W.succ) (ih3 W.succ) (ih4 W)
  (liftN_instN_hi .. ▸ ih5 W :)
  (liftN_instN_hi .. ▸ liftN_instN_hi .. ▸ ih6 W :)
State after:
no goals

State before:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (lam a (app (lift e) (VExpr.bvar 0))) k) (liftN n e k) (liftN n (forallE a B) k)
Tactic:
have := IsDefEqStrong.eta h1 h2 (ih1 W) (ih2 W.succ) ?_ (ih4 W) ?_
State after:
case eta.refine_3
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
this :
  IsDefEqStrong env U Γ' (lam (liftN n a k) (app (lift (liftN n e k)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))
⊢ IsDefEqStrong env U Γ' (liftN n (lam a (app (lift e) (VExpr.bvar 0))) k) (liftN n e k) (liftN n (forallE a B) k)

case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)

case eta.refine_2
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U (liftN n a k :: Γ') (lift (liftN n e k)) (lift (liftN n e k))
    (forallE (lift (liftN n a k)) (liftN 1 (liftN n B (k + 1)) 1))

State before:
case eta.refine_3
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
this :
  IsDefEqStrong env U Γ' (lam (liftN n a k) (app (lift (liftN n e k)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))
⊢ IsDefEqStrong env U Γ' (liftN n (lam a (app (lift e) (VExpr.bvar 0))) k) (liftN n e k) (liftN n (forallE a B) k)
Tactic:
simp [liftN]
State after:
case eta.refine_3
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
this :
  IsDefEqStrong env U Γ' (lam (liftN n a k) (app (lift (liftN n e k)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))
⊢ IsDefEqStrong env U Γ' (lam (liftN n a k) (app (liftN n (lift e) (k + 1)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))

State before:
case eta.refine_3
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
this :
  IsDefEqStrong env U Γ' (lam (liftN n a k) (app (lift (liftN n e k)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))
⊢ IsDefEqStrong env U Γ' (lam (liftN n a k) (app (liftN n (lift e) (k + 1)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))
Tactic:
rwa [← lift_liftN']
State after:
no goals

State before:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)
Tactic:
specialize ih3 W.succ.succ
State after:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)

State before:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)
Tactic:
have := liftN'_comm B n 1 (k+1) 1 (Nat.le_add_left ..)
State after:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
this : liftN 1 (liftN n B (k + 1)) 1 = liftN n (liftN 1 B 1) (1 + (k + 1))
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)

State before:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
this : liftN 1 (liftN n B (k + 1)) 1 = liftN n (liftN 1 B 1) (1 + (k + 1))
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)
Tactic:
rw [Nat.add_comm 1] at this
State after:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
this : liftN 1 (liftN n B (k + 1)) 1 = liftN n (liftN 1 B 1) (k + 1 + 1)
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)

State before:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
this : liftN 1 (liftN n B (k + 1)) 1 = liftN n (liftN 1 B 1) (k + 1 + 1)
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)
Tactic:
rwa [← this, ← lift_liftN'] at ih3
State after:
no goals

State before:
case eta.refine_2
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U (liftN n a k :: Γ') (lift (liftN n e k)) (lift (liftN n e k))
    (forallE (lift (liftN n a k)) (liftN 1 (liftN n B (k + 1)) 1))
Tactic:
have ih5 : IsDefEqStrong _ _ _ _ _ (liftN n (lift (forallE ..)) _) := ih5 W.succ
State after:
case eta.refine_2
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih5 :
  IsDefEqStrong env U (liftN n a k :: Γ') (liftN n (lift e) (k + 1)) (liftN n (lift e) (k + 1))
    (liftN n (lift (forallE a B)) (k + 1))
⊢ IsDefEqStrong env U (liftN n a k :: Γ') (lift (liftN n e k)) (lift (liftN n e k))
    (forallE (lift (liftN n a k)) (liftN 1 (liftN n B (k + 1)) 1))

State before:
case eta.refine_2
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih5 :
  IsDefEqStrong env U (liftN n a k :: Γ') (liftN n (lift e) (k + 1)) (liftN n (lift e) (k + 1))
    (liftN n (lift (forallE a B)) (k + 1))
⊢ IsDefEqStrong env U (liftN n a k :: Γ') (lift (liftN n e k)) (lift (liftN n e k))
    (forallE (lift (liftN n a k)) (liftN 1 (liftN n B (k + 1)) 1))
Tactic:
rwa [← lift_liftN', ← lift_liftN'] at ih5
State after:
no goals

State before:
case proofIrrel
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n p✝ k) (liftN n p✝ k) (liftN n (sort VLevel.zero) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n h✝ k) (liftN n h✝ k) (liftN n p✝ k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (liftN n h'✝ k) (liftN n h'✝ k) (liftN n p✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n h✝ k) (liftN n h'✝ k) (liftN n p✝ k)
Tactic:
exact .proofIrrel (ih1 W) (ih2 W) (ih3 W)
State after:
no goals

State before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k)
    (liftN n (instL ls✝ df✝.type) k)
Tactic:
have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
State after:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k)
    (liftN n (instL ls✝ df✝.type) k)

State before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k)
    (liftN n (instL ls✝ df✝.type) k)
Tactic:
simp [
  hA1.instL.liftN_eq (Nat.zero_le _),
  hA2.instL.liftN_eq (Nat.zero_le _),
  hA3.instL.liftN_eq (Nat.zero_le _)] at ih4 ih5 ⊢
State after:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
⊢ IsDefEqStrong env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)

State before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
h7 : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a_ih✝² :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.type) k) (liftN n (instL ls✝ df✝.type) k) (liftN n (sort u✝) k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.lhs) k)
        (liftN n (instL ls✝ df✝.type) k)
a_ih✝ :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k [] Γ' →
      IsDefEqStrong env U Γ' (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.rhs) k)
        (liftN n (instL ls✝ df✝.type) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEqStrong env U Γ' (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
⊢ IsDefEqStrong env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
Tactic:
exact IsDefEqStrong.extra h1 h2 h3 h4 h5 h6 h7 (ih4 W) (ih5 W)
State after:
no goals