proposition: Lemma Compose_compose_acc {E B} : forall transformer encode1 encode2 e0, @Compose.compose E B transformer encode1 encode2 e0 = @compose_acc E B transformer encode1 encode2 e0.
proof: Proof. intros; unfold compose_acc, Compose.compose, encode_continue. destruct (encode1 _); simpl; destruct (encode2 _); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics