proposition: Lemma EquivFormat_ComposeIf {S T} {cache : Cache} {monoid : Monoid T} : forall (format1 format1' format2 format2' : FormatM S T), EquivFormat format1 format1' -> EquivFormat format2 format2' -> EquivFormat (composeIf format1 format2) (composeIf format1' format2').
proof: Proof. unfold composeIf, Union_Format; split; intros; intros ? ? ; rewrite unfold_computes in H1; destruct_ex; intros; rewrite unfold_computes; exists x; revert H1; pattern x; apply IterateBoundedIndex.Iterate_Ensemble_BoundedIndex_equiv; simpl; repeat (apply IterateBoundedIndex.Build_prim_and; intros); eauto; simpl. apply H; apply H1. apply H0; apply H1. apply H; apply H1. apply H0; apply H1. Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats