proposition: Lemma nth_map_In : forall (A B : Set)(ls : list A)(f : A -> B) i defa defb, i < length ls -> nth i (map f ls) defa = f (nth i ls defb).
proof: Proof. induction ls; intuition; simpl in *. destruct i. lia. lia. destruct i. trivial. eapply IHls. lia. Qed.
imports: FCF.FCF Permutation