proposition: Lemma element_at_in : forall (x:A) l n, l[n] = Some x -> In x l.
proof: Proof. induction l; simpl; intros. discr. destruct n. inversion H. subst. auto. ded (IHl _ H). auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)