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