proposition: Lemma max_prefix_max l1 l2 k : k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix l1 l2).2.
proof: Proof. intros [l1' ->] [l2' ->]. by induction k; simpl; repeat case_decide; simpl; auto using prefix_nil, prefix_cons. Qed.
imports: stdpp(options)