Theorem SymOptionSuccEquiv.decode_inr

Modification history