proposition: Fact Forall_forall_map X (f : nat -> X) n l (P : X -> Prop) : l = map f (list_an 0 n) -> (forall i, i < n -> P (f i)) <-> Forall P l.
proof: Proof. intros Hl; rewrite Forall_forall. split. + intros H x; rewrite Hl, in_map_iff. intros (y & ? & H1). apply list_an_spec in H1; subst; apply H; lia. + intros H x Hx; apply H; rewrite Hl, in_map_iff. exists x; split; auto; apply list_an_spec; lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)