proposition: Lemma EquivFormat_reflexive {S T : Type} {cache : Cache} : forall (format : FormatM S T), EquivFormat format format.
proof: Proof. unfold EquivFormat; intros. reflexivity. 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