proposition: Lemma nth_lt_length : forall (A : Set)(ls : list A)(i : nat) a def, nth i ls def = a -> def <> a -> i < length ls.
proof: Proof. induction ls; intuition; simpl in *. destruct i; intuition. destruct i; subst. lia. apply ->Nat.succ_lt_mono. eauto. Qed.
imports: FCF.FCF Permutation