Prove some roundtrip properties

[Lysxia]

And other quality-of-life improvements (recursive deserialization!) Disabling tests for Coq <= 8.9 because a new test using fix does not work there.