proposition: Lemma EquivFormat_sym {S T} {cache : Cache} : forall (FormatSpec FormatSpec' : FormatM S T), EquivFormat FormatSpec FormatSpec' -> EquivFormat FormatSpec' FormatSpec.
proof: Proof. unfold EquivFormat, refineEquiv; intuition eauto; eapply H. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache