proposition: Lemma max_prefix_max_alt l1 l2 k1 k2 k3 k : max_prefix l1 l2 = (k1,k2,k3) → k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
proof: Proof. intro. pose proof (max_prefix_max l1 l2 k). by destruct (max_prefix l1 l2) as [[]?]; simplify_eq. Qed.
imports: stdpp(options)