proposition: Lemma dec_form_dep {b1 b2} phi1 phi2 : dec (eq_dep falsity_flag (@form _ _ _) b1 phi1 b2 phi2).
proof: Proof. Proof with subst; try (now left + (right; intros ? % eq_sigT_iff_eq_dep; resolve_existT; congruence)) using eq_dec_Funcs eq_dec_Preds eq_dec_quantop eq_dec_binop. unfold dec. revert phi2; induction phi1; intros; try destruct phi2. all: try now right; inversion 1. now left. - decide (b = b0)... decide (P = P0)... decide (t = t0)... right. intros [=] % eq_dep_falsity. resolve_existT. tauto. - decide (b = b1)... decide (b0 = b2)... destruct (IHphi1_1 phi2_1). + apply eq_dep_falsity in e as ->. destruct (IHphi1_2 phi2_2). * apply eq_dep_falsity in e as ->. now left. * right. rewrite eq_dep_falsity in *. intros [=]. now resolve_existT. + right. rewrite eq_dep_falsity in *. intros [=]. now repeat resolve_existT. - decide (b = b0)... decide (q = q0)... destruct (IHphi1 phi2). + apply eq_dep_falsity in e as ->. now left. + right. rewrite eq_dep_falsity in *. intros [=]. now resolve_existT. 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