proposition: Lemma bounded_comp_eq {ff} n phi : @bounded_comp ff n phi <-> @bounded ff n phi.
proof: Proof. Proof using sig_funcs_dec sig_preds_dec. induction phi in n|-*; cbn; (split; [intros H; econstructor|inversion 1; subst]). - easy. - induction t in H|-*; try easy. intros t' [->|Hin]%vec_cons_inv. + apply bounded_t_comp_correct. destruct H as [H1 H2]; apply H1. + apply IHt; try easy. destruct H as [H1 H2]; apply H2; easy. - apply inj_pair2_eq_dec in H4. 2: easy. subst. induction t in H3|-*; try easy. cbn. split. * apply bounded_t_comp_correct. apply H3. now left. * apply IHt. intros t' Ht'; apply H3. now right. - apply IHphi1. apply H. - apply IHphi2. apply H. - apply inj_pair2_eq_dec in H1. 2: decide equality. apply inj_pair2_eq_dec in H5. 2: decide equality. subst. split; try apply IHphi1; try apply IHphi2; easy. - now apply IHphi. - apply inj_pair2_eq_dec in H4. 2: decide equality. subst. apply IHphi. easy. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts