proposition: Lemma dec_predicate_dep ar1 ar2 (P1 : predicate ar1) (P2 : predicate ar2) : dec (eq_dep _ _ ar1 P1 ar2 P2).
proof: Proof. Proof using preds_eq_dec. destruct P1, P2. - destruct (PeanoNat.Nat.eq_dec ar ar0) as [->|]. destruct (PeanoNat.Nat.eq_dec n n0) as [->|]. left; now apply predicate_eq_dep. right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality. right; intros H%eq_sigT_iff_eq_dep; congruence. - destruct (PeanoNat.Nat.eq_dec ar (ar_preds P)) as [->|]. right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality. right. intros H%eq_sigT_iff_eq_dep. inversion H. - destruct (PeanoNat.Nat.eq_dec ar (ar_preds P)) as [->|]. right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality. right. intros H%eq_sigT_iff_eq_dep. inversion H. - destruct (preds_eq_dec P P0) as [->|]. left; now apply predicate_eq_dep. right. now intros [=]%eq_sigT_iff_eq_dep. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec