proposition: Lemma Nth_inbound : forall n l x, Nth n l x -> n < length l.
proof: Proof. Proof using. intros n. induction n; introv H; inverts H; rew_list in *. { math. } { forwards*: IHn. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)