proposition: Lemma cleanup_aligned_encoder_AlignedEncodeList {cache: Cache} {A: Type}: forall (encA encA': forall sz, AlignedEncodeM sz) sz (f: AlignedEncodeM sz), (forall v idx r ch, encA sz v idx r ch = encA' sz v idx r ch) -> (forall r v idx ch, @AlignedEncodeList cache A encA' sz v idx r ch = f v idx r ch) -> (forall r v idx ch, @AlignedEncodeList cache A encA sz v idx r ch = f v idx r ch).
proof: Proof. intros; erewrite AlignedEncodeList_morphism; eauto. 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