proposition: Lemma term_ind (p : term -> Prop) : (forall n, p (var_indi n)) -> (forall ar n v (IH : Forall p v), p (func (var_func n ar) v)) -> (forall f v (IH : Forall p v), p (func (sym f) v)) -> forall t, p t.
proof: Proof. intros H1 H2 H3. fix term_ind 1. destruct t. - apply H1. - destruct f. + apply H2. induction v. * constructor. * constructor. apply term_ind. exact IHv. + apply H3. induction v. * constructor. * 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