proposition: Lemma term_rect' (p : term -> Type) : (forall x, p (var x)) -> (forall F v, (ForallT p v) -> p (@func F v)) -> forall (t : term), p t.
proof: Proof. intros f1 f2. fix strong_term_ind' 1. destruct t as [n|F v]. - apply f1. - apply f2. induction v. + econstructor. + econstructor. now eapply strong_term_ind'. eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)