proposition: Lemma find_first_Some_bound : forall l x, find_first l = Some x -> x < length l.
proof: Proof. induction l; intros. simpl in H; discr. simpl in H. destruct (P_dec a). inversion H; subst. simpl; lia. destruct (find_first l). inversion H; subst. simpl; apply NatCompat.lt_n_S; apply IHl; auto. discr. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)