proposition: Lemma lookupIndex_lt_length : forall (A : Set)(eqd : eq_dec A)(ls : list A) a def, In a ls -> lookupIndex eqd ls a def < length ls.
proof: Proof. induction ls; intuition; simpl in *; intuition; subst. destruct (eqd a0 a0); subst; intuition. destruct (eqd a0 a); subst. lia. apply ->Nat.succ_lt_mono. eapply IHls. trivial. Qed.
imports: FCF.FCF Permutation