α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (↑t) (d :: ds)
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (i :: is) (d :: ds)
rw [← hiis]
no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (↑t) (d :: ds)
exact t.2
no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x x_1 => x < x_1) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x x_1 => x < x_1) is ds
⊢ slice x i hid { val := is, property := hisds } = slice y i hid { val := is, property := hisds }
rw [h]