cases B
case mk
α : Type u_1
B : Array α
data✝ : List α
⊢ { data := data✝ } = B ↔ { data := data✝ }.data = B.data
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
⊢ { data := data✝¹ } = { data := data✝ } ↔ { data := data✝¹ }.data = { data := data✝ }.data