proposition: Lemma function_eq_dep ar (f1 f2 : function ar) : eq_dep _ _ ar f1 ar f2 <-> f1 = f2.
proof: Proof. rewrite <- eq_sigT_iff_eq_dep. split. - intros H%Eqdep_dec.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