proposition: Lemma index_of_index_length' : forall l n i, index n i -> n = length l -> index l i.
proof: Proof. Proof using. intros. subst. rewrite~ index_eq_index_length. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)