-- should make this case better
= mkAppCoercion (mkSymCoercion co1) (mkSymCoercion co2)
| Just (co1, co2) <- splitTransCoercion_maybe co
-- should make this case better
= mkAppCoercion (mkSymCoercion co1) (mkSymCoercion co2)
| Just (co1, co2) <- splitTransCoercion_maybe co