proposition: Lemma ith_eq : forall l i (hi : i < length l) j (hj : j < length l), i = j -> ith hi = ith hj.
proof: Proof. intros. subst j. rewrite (lt_unique hi hj). refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)