proposition: Lemma composeIf_subformat_correct_prefix {S T} {cache : Cache} (monoid : Monoid T) (formatT formatE : FormatM S T) (subformatT subformatE : FormatM S T) (subformat_OK1 : Prefix_Format monoid formatT subformatT) (subformat_OK2 : Prefix_Format monoid formatE subformatE) : Prefix_Format monoid (composeIf formatT formatE) (composeIf subformatT subformatE).
proof: Proof. unfold Prefix_Format in *; intros. apply composeIf_format_elim in H. destruct H. edestruct subformat_OK1; eauto. destruct_ex. eexists _, _, _; intuition eauto. eauto using composeIf_format_inj1. edestruct subformat_OK2; eauto. destruct_ex. eexists _, _, _; intuition eauto. eauto using composeIf_format_inj2. Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats