ISE

[ice1000]

def ++-assoc {xs ys zs : FMSet A} : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs elim xs
| [] => refl
| x :] xs' => pmap (x :]) ++-assoc
| comm x y xs' i => pmap (comm x y) {??}

[ice1000]

Wrong:

def ++-assoc {xs ys zs : FMSet A} : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs elim xs
| [] => refl
| x :] xs' => pmap (x :]) ++-assoc
| comm x y xs' i => {??}