no goals
α : Type u_1
β : Type u_2
γ : Type ?u.465908
δ : Type ?u.465911
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ↑card s = ↑card t
induction h <;> simp [*]