proposition: Lemma element_at_in2 : forall (x:A) l n, l[n] = Some x -> In x l /\ n < length l.
proof: Proof. induction l; intros; simpl in H; try discr. destruct n. inversion H; subst; simpl; auto with *. ded (IHl n H). intuition; simpl; lia. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)