rw [← mul_mk, ← mul_mk]
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk (L₁ ++ L₃) = mk (L₂ ++ L₃)
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk L₁ * mk L₃ = mk L₂ * mk L₃