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