proposition: Lemma Forall_in {X n} (p : X -> Prop) (v : t X n) : Forall p v <-> forall x, In x v -> p x.
proof: Proof. induction v. easy. split. - intros H1 x. assert (HIn : forall {n: nat} (x : X) (xs : Vector.t X n), In x xs -> match xs with | Vector.nil _ => False | cons _ y _ ys => y = x \/ In x ys end). { now intros ??? []; [left|right]. } intros ?%HIn. firstorder (now subst). - intros H. split. apply H. constructor. apply IHv. intros x H1. apply H. now constructor. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec