proposition: Lemma term_ind (p : term -> Prop) : (forall x, p (var x)) -> (forall F v (IH : forall t, In t v -> p t), p (func F v)) -> forall (t : term), p t.
proof: Proof. intros f1 f2. eapply term_rect'. - apply f1. - intros. apply f2. intros t. induction 1; inversion X; subst; eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)