proposition: Lemma composeIf_format_elim {S T} {cache : Cache} (monoid : Monoid T) s env t env' (formatT formatE : FormatM S T) : composeIf formatT formatE s env ∋ (t, env') -> formatT s env ∋ (t, env') \/ formatE s env ∋ (t, env').
proof: Proof. unfold composeIf, Union_Format. rewrite unfold_computes. intros [? ?]. revert H. apply (Fin.caseS' x). eauto. clear x. intros x. apply (Fin.caseS' x). eauto. clear x. intros x. apply Fin.case0; auto. Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats