proposition: Lemma map_nth_seq A (f : nat -> A) a d l (EQ: forall i (LTi : i < length l), f (a + i) = nth i l d) : map f (seq a (length l)) = l.
proof: Proof. revert a EQ; induction l; ins; f_equal. rewrite <- (EQ 0); try rewrite Nat.add_0_r; ins; lia. eapply IHl; ins; rewrite <- Nat.add_succ_r. eapply (EQ (S i)); lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation