proposition: Lemma join_reshape szs l : sum_list szs = length l → mjoin (reshape szs l) = l.
proof: Proof. revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|]. by rewrite IH, take_drop by (rewrite drop_length; lia). Qed.
imports: stdpp(options)