proposition: Lemma term_rect (p : term -> Type) : (forall x, p (var x)) -> (forall F v, (forall t, InT 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. induction v. + intros t H; exfalso; apply H. + intros t [->|H]; cbn in *; destruct X; eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)