proposition: Lemma cleanup_aligned_encoder_bind {cache S2}: forall (sz : nat) (v : t Core.char sz) idx (r : S2) ch, forall (f f' g g': @AlignedEncodeM cache S2 sz), (forall v idx r ch, g v idx r ch = g' v idx r ch) -> (forall v idx r ch, f v idx r ch = f' v idx r ch) -> (AppendAlignedEncodeM f g) v idx r ch = (AppendAlignedEncodeM f' g') v idx r ch.
proof: Proof. compute; intros * Hg Hf. rewrite Hf; destruct (f' _ _ _ _); congruence. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.AlignedAutomation Fiat.Narcissus.BinLib Fiat.Narcissus.Formats Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.BaseFormats Fiat.Common.EnumType Fiat.Narcissus.Formats.EnumOpt