proposition: Lemma cleanup_aligned_encoder_bind_projection {cache S1 S2 sz}: forall (f f': @AlignedEncodeM cache S2 sz) (h: @AlignedEncodeM cache S1 sz) proj, (forall v idx r1 ch, f' v idx (proj r1) ch = h v idx r1 ch) -> (forall v idx r2 ch, f v idx r2 ch = f' v idx r2 ch) -> forall (v : t Core.char sz) idx (r1: S1) r2 ch, r2 = proj r1 -> f v idx r2 ch = h v idx r1 ch.
proof: Proof. 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