proposition: Theorem in_ex_nth: forall (a b: A) l, In a l <-> exists n, n < length l /\ a = nth n l b.
proof: Proof. intros a b l. split; intros H. - pose proof (In_nth l a b H). destruct H0 as [n [H1 H2]]. exists n; auto. - destruct H as [n [H1 H2]]. pose proof (nth_In _ b H1); subst; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat