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