proposition: Lemma prefix_length_eq l1 l2 : l1 `prefix_of` l2 → length l2 ≤ length l1 → l1 = l2.
proof: Proof. intros Hprefix Hlen. assert (length l1 = length l2). { apply prefix_length in Hprefix. lia. } eapply list_eq_same_length with (length l1); [done..|]. intros i x y _ ??. assert (l2 !! i = Some x) by eauto using prefix_lookup_Some. congruence. Qed.
imports: stdpp(options)