proposition: Lemma take_full_length : forall l, take (length l) l = l.
proof: Proof. Proof using. intros. unfold take, length. rew_to_nat_nonneg~. apply LibList.take_full_length. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)