proposition: Lemma prefix_cons_cons_eq: forall x xs1 xs2, prefix (x :: xs1) (x :: xs2) = prefix xs1 xs2.
proof: Proof. Proof using. intros. extens. split. { eapply prefix_cons_cons_inverse. } { eapply prefix_cons_cons. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)