proposition: Lemma index_rev_eq : forall l i, index (rev l) i = index l i.
proof: Proof. Proof using. extens. intros. now rewrite index_eq_index_length, length_rev, index_eq_index_length. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)