proposition: Lemma Forall_map {X Y n} (p : Y -> Prop) (f : X -> Y) (v : t X n) : Forall p (map f v) <-> Forall (fun x => p (f x)) v.
proof: Proof. induction v; firstorder. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec