ds₁ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is ds₁
⊢ ↑(cast (_ : HolorIndex ds₁ = HolorIndex ds₁) { val := is, property := h }) = is
ds₁ ds₂ ds₃ is : List ℕ
eq : ds₁ = ds₂
h : Forall₂ (fun x x_1 => x < x_1) is ds₁
⊢ ↑(cast (_ : HolorIndex ds₁ = HolorIndex ds₂) { val := is, property := h }) = is
subst eq
no goals
ds₁ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is ds₁
⊢ ↑(cast (_ : HolorIndex ds₁ = HolorIndex ds₁) { val := is, property := h }) = is
rfl