proposition: Lemma prefix_weak_total l1 l2 l3 : l1 `prefix_of` l3 → l2 `prefix_of` l3 → l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
proof: Proof. intros [k1 H1] [k2 H2]. rewrite H2 in H1. apply app_eq_inv in H1 as [(k&?&?)|(k&?&?)]; [left|right]; exists k; eauto. Qed.
imports: stdpp(options)