proposition: Lemma predicate_eq_dep ar (P1 P2 : predicate ar) : eq_dep _ _ ar P1 ar P2 <-> P1 = P2.
proof: Proof. rewrite <- eq_sigT_iff_eq_dep. split. - intros H%inj_pair2_eq_dec. exact H. decide equality. - now intros ->. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec