proposition: Lemma ith_In : forall l i (h : i < length l), In (ith h) l.
proof: Proof. induction l; simpl; intros. lia. destruct i. auto. right. apply IHl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)