proposition: Lemma element_at_exists : forall l p, p < length l <-> ex (fun a => l[p] = Some a).
proof: Proof. intro l; induction l as [ | h t IHl]. simpl; intro p; split; intro H; [inversion H | inversion H as [x Hx]]. inversion Hx. simpl; intro p; split. intro Hp; destruct p as [ | p]. exists h; trivial. assert (Hp' : p < length t). gen Hp; auto with arith. elim (IHl p); intros H1 H2. elim (H1 Hp'); intros a Ha; exists a; trivial. destruct p as [ | p]; intro H. auto with arith. elim (IHl p); intros H1 H2. gen (H2 H); auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)