proposition: Lemma set_seq_add_L `{!LeibnizEquiv C} start len1 len2 : set_seq (C:=C) start (len1 + len2) = set_seq start len1 ∪ set_seq (start + len1) len2.
proof: Proof. unfold_leibniz. apply set_seq_add. Qed.
imports: stdpp(finite) stdpp(options)