proposition: Theorem firstIndexOf_in_lt : forall (A : Set)(eqd : eq_dec A)(ls : list A)(a : A)(def : nat), In a ls -> firstIndexOf eqd ls a def < length ls.
proof: Proof. induction ls; intuition; simpl in *; intuition. subst. destruct (eqd a0 a0); subst. lia. intuition. destruct (eqd a0 a); subst. lia. apply ->Nat.succ_lt_mono. eauto. Qed.
imports: FCF.FCF