proposition: Lemma composeIf_format_inj2 {S T} {cache : Cache} (monoid : Monoid T) s env t env' (formatT formatE : FormatM S T) : formatE s env ∋ (t, env') -> composeIf formatT formatE s env ∋ (t, env').
proof: Proof. intros. unfold composeIf, Union_Format. rewrite unfold_computes. exists (Fin.FS Fin.F1). eauto. Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats