proposition: Lemma read_take : forall (IA:Inhab A) l s i, s <= length l -> index s i -> (take s l)[i] = l[i].
proof: Proof. Proof using. introv Hs Hi. rew_index in *. lets (l'&Hl&Hl'): take_spec s l. { math. } rewrite Hl' at 2. rewrite read_app. case_if*. { false. rewrite length_take_nonneg in C; try math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)