simp only [List.length_append, List.length_map]
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (List.map Sum.inl (elems α) ++ List.map Sum.inr (elems β)) = card α + card β
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (elems α) + List.length (elems β) = card α + card β