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