proposition: Lemma refineEquiv_ComposeIf {S T} {cache : Cache} {monoid : Monoid T} : forall (format1 format1' format2 format2' : FormatM S T), (forall s env, refineEquiv (format1 s env) (format1' s env)) -> (forall s env, refineEquiv (format2 s env) (format2' s env)) -> (forall s env, refineEquiv (composeIf format1 format2 s env) (composeIf format1' format2' s env)).
proof: Proof. intros; eapply EquivFormat_ComposeIf; eauto. Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats