proposition: Lemma seq_eq_cons start len x l : seq start len = x :: l <-> match len with 0 => False | S len' => start = x /\ seq (S x) len' = l end.
proof: Proof. desf; split; ins; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation