proposition: Lemma index_app_eq : forall l l' i, index (l++l') i = (If i < length l then index l i else index l' (i - length l)).
proof: Proof. Proof using. intros. extens. rew_index. iff; case_if; math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)