proposition: Lemma index_of_inbound : forall l i, 0 <= i < length l -> index l i.
proof: Proof. Proof using. intros. rewrite~ index_eq_inbound. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)