proposition: Lemma vec_all_dec X n (v : vec X n) (P : X -> Prop) : (forall x, InT x v -> dec (P x)) -> dec (forall x, In x v -> P x).
proof: Proof. induction v; intros H. - left. intros x. inversion 1. - destruct (H h) as [H1|H1], IHv as [H2|H2]; try now left. + intros x Hx. apply H. now right. + intros x Hx. apply H. now right. + left. intros x [<-| Hx] % vec_cons_inv; intuition. + right. contradict H2. intros x Hx. apply H2. now right. + intros x Hx. apply H. now right. + right. contradict H1. apply H1. now left. + right. contradict H1. apply H1. now left. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts