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

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
H : IsDefEqStrong env U Γ e1 e2 A
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ) (VExpr.instL ls e1) (VExpr.instL ls e2) (VExpr.instL ls A)
Tactic:
induction H with
| bvar h _ _ ih =>
  exact .bvar h.instL (.inst hls) ih
| constDF h1 h2 h3 h4 h5 _ _ _ _ _ ih1 ih2 ih3 ih4 =>
  simp [VExpr.instL, VExpr.instL_instL] at ih1 ih2 ih3 ih4 ⊢
  exact .constDF h1
    (by simp [h2, VLevel.WF.inst hls]) (by simp [h3, VLevel.WF.inst hls]) (by simp [h4])
    (by simpa using h5.imp fun _ _ => VLevel.inst_congr_l) (.inst hls) ih1 ih2 ih3 ih4
| symm _ ih => exact .symm ih
| trans _ _ ih1 ih2 => exact .trans ih1 ih2
| sortDF _ _ h3 =>
  exact .sortDF (VLevel.WF.inst hls) (VLevel.WF.inst hls) (VLevel.inst_congr_l h3)
| appDF _ _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact instL_instN ▸ .appDF (.inst hls) (.inst hls)
    ih1 ih2 ih3 ih4 (instL_instN ▸ instL_instN ▸ ih5)
| lamDF _ _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact .lamDF (.inst hls) (.inst hls) ih1 ih2 ih3 ih4 ih5
| forallEDF _ _ _ _ _ ih1 ih2 ih3 =>
  exact .forallEDF (.inst hls) (.inst hls) ih1 ih2 ih3
| defeqDF _ _ _ ih1 ih2 =>
  exact .defeqDF (.inst hls) ih1 ih2
| beta _ _ _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 ih6 =>
  simpa using .beta (.inst hls) (.inst hls) ih1 ih2 ih3 ih4
    (by simpa using ih5) (by simpa using ih6)
| eta _ _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  simpa [VExpr.instL] using .eta (.inst hls) (.inst hls) ih1 ih2
    (by simpa using ih3) ih4 (by simpa [VExpr.instL] using ih5)
| proofIrrel _ _ _ ih1 ih2 ih3 =>
  exact .proofIrrel ih1 ih2 ih3
| extra h1 h2 h3 _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  simp [VExpr.instL, VExpr.instL_instL] at ih1 ih2 ih3 ih4 ih5 ⊢
  exact .extra h1 (by simp [h2, VLevel.WF.inst hls]) (by simp [h3])
    (.inst hls) ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
case bvar
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
u✝ : VLevel
h : Lookup Γ✝ i✝ A✝
a✝¹ : VLevel.WF U u✝
a✝ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
ih :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.bvar i✝)) (VExpr.instL ls (VExpr.bvar i✝))
    (VExpr.instL ls A✝)
Tactic:
exact .bvar h.instL (.inst hls) ih
State after:
no goals

State before:
case constDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls✝ ci✝.type)) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type)) (VExpr.instL ls (sort u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls✝ ci✝.type)) (VExpr.instL ls (sort u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type)) (VExpr.instL ls (sort u✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (const c✝ ls✝)) (VExpr.instL ls (const c✝ ls'✝))
    (VExpr.instL ls (VExpr.instL ls✝ ci✝.type))
Tactic:
simp [VExpr.instL, VExpr.instL_instL] at ih1 ih2 ih3 ih4 ⊢
State after:
case constDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (const c✝ (List.map (VLevel.inst ls) ls✝))
    (const c✝ (List.map (VLevel.inst ls) ls'✝)) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)

State before:
case constDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (const c✝ (List.map (VLevel.inst ls) ls✝))
    (const c✝ (List.map (VLevel.inst ls) ls'✝)) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
Tactic:
exact .constDF h1
  (by simp [h2, VLevel.WF.inst hls]) (by simp [h3, VLevel.WF.inst hls]) (by simp [h4])
  (by simpa using h5.imp fun _ _ => VLevel.inst_congr_l) (.inst hls) ih1 ih2 ih3 ih4
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls✝ → VLevel.WF U' l
Tactic:
simp [h2, VLevel.WF.inst hls]
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls'✝ → VLevel.WF U' l
Tactic:
simp [h3, VLevel.WF.inst hls]
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ List.length (List.map (VLevel.inst ls) ls✝) = ci✝.uvars
Tactic:
simp [h4]
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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'✝
a✝⁴ : VLevel.WF U 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✝¹ : 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✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ List.Forall₂ (fun x x_1 => x ≈ x_1) (List.map (VLevel.inst ls) ls✝) (List.map (VLevel.inst ls) ls'✝)
Tactic:
simpa using h5.imp fun _ _ => VLevel.inst_congr_l
State after:
no goals

State before:
case symm
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e✝) (VExpr.instL ls A✝)
Tactic:
exact .symm ih
State after:
no goals

State before:
case trans
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e₁✝) (VExpr.instL ls e₂✝) (VExpr.instL ls A✝)
ih2 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e₂✝) (VExpr.instL ls e₃✝) (VExpr.instL ls A✝)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e₁✝) (VExpr.instL ls e₃✝) (VExpr.instL ls A✝)
Tactic:
exact .trans ih1 ih2
State after:
no goals

State before:
case sortDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
a✝¹ : VLevel.WF U l✝
a✝ : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (sort l✝)) (VExpr.instL ls (sort l'✝))
    (VExpr.instL ls (sort (VLevel.succ l✝)))
Tactic:
exact .sortDF (VLevel.WF.inst hls) (VLevel.WF.inst hls) (VLevel.inst_congr_l h3)
State after:
no goals

State before:
case appDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls f✝) (VExpr.instL ls f'✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih4 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls a✝⁷) (VExpr.instL ls a'✝) (VExpr.instL ls A✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst B✝ a✝⁷)) (VExpr.instL ls (inst B✝ a'✝))
    (VExpr.instL ls (sort v✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (app f✝ a✝⁷)) (VExpr.instL ls (app f'✝ a'✝))
    (VExpr.instL ls (inst B✝ a✝⁷))
Tactic:
exact instL_instN ▸ .appDF (.inst hls) (.inst hls)
  ih1 ih2 ih3 ih4 (instL_instN ▸ instL_instN ▸ ih5)
State after:
no goals

State before:
case lamDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A'✝)
    (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A'✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls body✝) (VExpr.instL ls body'✝)
    (VExpr.instL ls B✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A'✝ :: Γ✝)) (VExpr.instL ls body✝) (VExpr.instL ls body'✝)
    (VExpr.instL ls B✝)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (lam A✝ body✝)) (VExpr.instL ls (lam A'✝ body'✝))
    (VExpr.instL ls (forallE A✝ B✝))
Tactic:
exact .lamDF (.inst hls) (.inst hls) ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
case forallEDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝⁴ : VLevel.WF U u✝
a✝³ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A'✝)
    (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls body✝) (VExpr.instL ls body'✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A'✝ :: Γ✝)) (VExpr.instL ls body✝) (VExpr.instL ls body'✝)
    (VExpr.instL ls (sort v✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (forallE A✝ body✝))
    (VExpr.instL ls (forallE A'✝ body'✝)) (VExpr.instL ls (sort (VLevel.imax u✝ v✝)))
Tactic:
exact .forallEDF (.inst hls) (.inst hls) ih1 ih2 ih3
State after:
no goals

State before:
case defeqDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls B✝) (VExpr.instL ls (sort u✝))
ih2 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e1✝) (VExpr.instL ls e2✝) (VExpr.instL ls A✝)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e1✝) (VExpr.instL ls e2✝) (VExpr.instL ls B✝)
Tactic:
exact .defeqDF (.inst hls) ih1 ih2
State after:
no goals

State before:
case beta
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls B✝)
ih4 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst B✝ e'✝)) (VExpr.instL ls (inst B✝ e'✝))
    (VExpr.instL ls (sort v✝))
ih6 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst e✝ e'✝)) (VExpr.instL ls (inst e✝ e'✝))
    (VExpr.instL ls (inst B✝ e'✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (app (lam A✝ e✝) e'✝))
    (VExpr.instL ls (inst e✝ e'✝)) (VExpr.instL ls (inst B✝ e'✝))
Tactic:
simpa using .beta (.inst hls) (.inst hls) ih1 ih2 ih3 ih4
  (by simpa using ih5) (by simpa using ih6)
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls B✝)
ih4 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst B✝ e'✝)) (VExpr.instL ls (inst B✝ e'✝))
    (VExpr.instL ls (sort v✝))
ih6 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst e✝ e'✝)) (VExpr.instL ls (inst e✝ e'✝))
    (VExpr.instL ls (inst B✝ e'✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (inst (VExpr.instL ls B✝) (VExpr.instL ls e'✝))
    (inst (VExpr.instL ls B✝) (VExpr.instL ls e'✝)) (sort (VLevel.inst ls v✝))
Tactic:
simpa using ih5
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls B✝)
ih4 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst B✝ e'✝)) (VExpr.instL ls (inst B✝ e'✝))
    (VExpr.instL ls (sort v✝))
ih6 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst e✝ e'✝)) (VExpr.instL ls (inst e✝ e'✝))
    (VExpr.instL ls (inst B✝ e'✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (inst (VExpr.instL ls e✝) (VExpr.instL ls e'✝))
    (inst (VExpr.instL ls e✝) (VExpr.instL ls e'✝)) (inst (VExpr.instL ls B✝) (VExpr.instL ls e'✝))
Tactic:
simpa using ih6
State after:
no goals

State before:
case eta
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (lift A✝ :: A✝ :: Γ✝)) (VExpr.instL ls (liftN 1 B✝ 1))
    (VExpr.instL ls (liftN 1 B✝ 1)) (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls (lift e✝)) (VExpr.instL ls (lift e✝))
    (VExpr.instL ls (forallE (lift A✝) (liftN 1 B✝ 1)))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (lam A✝ (app (lift e✝) (VExpr.bvar 0))))
    (VExpr.instL ls e✝) (VExpr.instL ls (forallE A✝ B✝))
Tactic:
simpa [VExpr.instL] using .eta (.inst hls) (.inst hls) ih1 ih2
  (by simpa using ih3) ih4 (by simpa [VExpr.instL] using ih5)
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (lift A✝ :: A✝ :: Γ✝)) (VExpr.instL ls (liftN 1 B✝ 1))
    (VExpr.instL ls (liftN 1 B✝ 1)) (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls (lift e✝)) (VExpr.instL ls (lift e✝))
    (VExpr.instL ls (forallE (lift A✝) (liftN 1 B✝ 1)))
⊢ IsDefEqStrong env U' (lift (VExpr.instL ls A✝) :: VExpr.instL ls A✝ :: List.map (VExpr.instL ls) Γ✝)
    (liftN 1 (VExpr.instL ls B✝) 1) (liftN 1 (VExpr.instL ls B✝) 1) (sort (VLevel.inst ls v✝))
Tactic:
simpa using ih3
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (lift A✝ :: A✝ :: Γ✝)) (VExpr.instL ls (liftN 1 B✝ 1))
    (VExpr.instL ls (liftN 1 B✝ 1)) (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls (lift e✝)) (VExpr.instL ls (lift e✝))
    (VExpr.instL ls (forallE (lift A✝) (liftN 1 B✝ 1)))
⊢ IsDefEqStrong env U' (VExpr.instL ls A✝ :: List.map (VExpr.instL ls) Γ✝) (lift (VExpr.instL ls e✝))
    (lift (VExpr.instL ls e✝)) (forallE (lift (VExpr.instL ls A✝)) (liftN 1 (VExpr.instL ls B✝) 1))
Tactic:
simpa [VExpr.instL] using ih5
State after:
no goals

State before:
case proofIrrel
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls p✝) (VExpr.instL ls p✝)
    (VExpr.instL ls (sort VLevel.zero))
ih2 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h✝) (VExpr.instL ls h✝) (VExpr.instL ls p✝)
ih3 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h'✝) (VExpr.instL ls h'✝) (VExpr.instL ls p✝)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h✝) (VExpr.instL ls h'✝) (VExpr.instL ls p✝)
Tactic:
exact .proofIrrel ih1 ih2 ih3
State after:
no goals

State before:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
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✝¹ : 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)
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.type)) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
Tactic:
simp [VExpr.instL, VExpr.instL_instL] at ih1 ih2 ih3 ih4 ih5 ⊢
State after:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
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✝¹ : 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)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih3 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)

State before:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
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✝¹ : 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)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih3 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
Tactic:
exact .extra h1 (by simp [h2, VLevel.WF.inst hls]) (by simp [h3])
  (.inst hls) ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
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✝¹ : 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)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih3 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls✝ → VLevel.WF U' l
Tactic:
simp [h2, VLevel.WF.inst hls]
State after:
no goals

State before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
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✝¹ : 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)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih3 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
⊢ List.length (List.map (VLevel.inst ls) ls✝) = df✝.uvars
Tactic:
simp [h3]
State after:
no goals