fact: Definition composeIf {S T} {cache : Cache} {monoid : Monoid T} (formatT : FormatM S T) (formatE : FormatM S T) := Union_Format (Vector.cons _ formatT _ (Vector.cons _ formatE _ (Vector.nil _))).
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats