proposition: Lemma in_exists_element_at : forall l a, In a l -> ex (fun p => l[p] = Some a).
proof: Proof. intro l; induction l as [ | h t IHl]; intros a a_in_l. inversion a_in_l. elim a_in_l; clear a_in_l; intro a_in_l. exists 0; subst; trivial. elim (IHl a a_in_l); intros p Hp. exists (S p); simpl; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)