proposition: Lemma prefix_full_inv : forall xs ys, length xs = length ys -> prefix xs ys -> xs = ys.
proof: Proof. Proof using. introv Hl (zs,Hzs). asserts E : (zs = nil). { destruct zs; try easy. apply (f_equal (length (A:=A))) in Hzs. rew_list in Hzs. math. } subst. rew_list*. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)