proposition: Lemma dec_vec_in X n (v : vec X n) : (forall x, InT x v -> forall y, dec (x = y)) -> forall v', dec (v = v').
proof: Proof. Proof with subst; try (now left + (right; intros[=])). intros Hv. induction v; intros v'. - pattern v'. apply Vector.case0... - apply (Vector.caseS' v'). clear v'. intros h0 v'. destruct (Hv h (inl eq_refl) h0)... edestruct IHv. + intros x H. apply Hv. now right. + left. f_equal. apply e. + right. intros H. inversion H. resolve_existT. tauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts