proposition: Lemma AlignedEncodeList_morphism {cache: Cache} {A: Type}: forall (encA encA': forall sz, AlignedEncodeM sz) 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 = @AlignedEncodeList cache A encA' sz v idx r ch).
proof: Proof. intros * Heq; induction r; simpl; intros. - reflexivity. - rewrite Heq; destruct (encA' _ _ _ _ _); simpl; 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