proposition: Lemma map_S_seq {A} (f : nat -> A) x y : map (fun i => f (S i)) (seq x y) = map f (seq (S x) y).
proof: Proof. clear; revert x; induction y; intros. { reflexivity. } { simpl. rewrite IHy; reflexivity. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts