proposition: Lemma take_full_length : forall l, take (length l) l = l.
proof: Proof. Proof using. intros. lets H: (@take_prefix_length l nil). rew_list~ in H. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)