proposition: Lemma of_map_L P n (f : N n -> elts P) : surjective f -> P [=] of_list (map (elt_val o f) (L n)).
proof: Proof. intro f_surj. set (g := elt_val o f). rewrite equiv_subset2. split; intros x_val x. unfold mem, of_list. destruct (f_surj (elt x)) as [[k_val k] e]. apply sig_eq in e; simpl in e. subst. change (In (g (N_ k)) (map g (L n))). apply in_map. apply In_L. unfold mem, of_list in x. destruct (in_map_elim x) as [k [k1 k2]]. subst. unfold g, comp. destruct (f k) as [y_val y]. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)