proposition: Lemma cleanup_aligned_encoder_distribute {cache S1 S2}: forall (sz : nat) (r : S1) (v : t Core.char sz) ch idx, forall (f1 f2: @AlignedEncodeM cache S2 sz) (g: @AlignedEncodeM cache S1 sz) x proj, (AppendAlignedEncodeM (fun v idx r => f1 v idx (proj r)) (AppendAlignedEncodeM (fun v idx r => f2 v idx (proj r)) g)) v idx r ch = x -> (AppendAlignedEncodeM (fun v idx r => (AppendAlignedEncodeM f1 f2) v idx (proj r)) g) v idx r ch = x.
proof: Proof. compute; intros; destruct (f1 _ _ _ _); [ destruct (f2 _ _ _ _) | ]; 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