proposition: Lemma term_ind' (p : term -> Prop) : (forall n, p (var_indi n)) -> (forall ar (f : function ar) v (IH : Forall p v), p (func f v)) -> forall t, p t.
proof: Proof. intros H1 H2. fix term_ind' 1. destruct t. - apply H1. - apply H2. clear f. induction v; constructor. apply term_ind'. exact IHv. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec