Currently, we can't prove that primStringToList and primStringFromList, conversions between String and List Char, are mutually inverse, although we have their injectivities, primStringToListInjective and primStringFromListInjective.

I believe this mutual inverse is useful. Can we add a primitive lemma like the following?

primStringFromToListId : ∀ a → primStringFromList (primStringToList a) ≡ a

The opposite side

primStringToFromListId : ∀ a → primStringToList (primStringFromList a) ≡ a

can be proved by combining primStringFromToListId with the injectivity primStringFromListInjective.

Or as another option, we can add both primStringFromToListId and primStringToFromListId as a primitive.
Then the injectivities primStringToListInjective and primStringFromListInjective are derivable.