no goals
α : Type u_1
β : Sort ?u.54436
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
as bs : List α
h : Disjoint as bs
⊢ card (List.union as bs) = card as + card bs
rw [card_eq_of_equiv (union_equiv_append as bs), card_append_disjoint h]