proposition: Lemma Forall_ext_in {X n} (p q : X -> Prop) (v : t X n) : (forall x, In x v -> p x -> q x) -> Forall p v -> Forall q v.
proof: Proof. intros H1 H2. induction v; cbn. easy. split. apply H1. constructor. apply H2. apply IHv. intros x H3. apply H1. now constructor. apply H2. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec