proposition: Lemma list_prod_in X Y (x : X * Y) A B : x el (list_prod A B) -> exists a b, x = (a , b) /\ a el A /\ b el B.
proof: Proof. induction A; cbn. - intros []. - intros [H | H] % in_app_or. 2: firstorder. apply in_map_iff in H as (y & <- & Hel). exists a, y. tauto. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List