{σ : Signature} (C : Carriers σ) (P : Sort σ -> Type) (vs : forall (s : Sort σ), C s -> P s) (os : forall (u : Symbol σ) (c : DomOperation (CarriersTermAlgebra C) (σ u)), (forall i : Arity (σ u), P (sorts_dom (σ u) i)) -> P (sort_cod (σ u))) (s : Sort σ) (T : CarriersTermAlgebra C s) : P s := CarriersTermAlgebra_ind C (fun s _ => P s) vs os s T.
Require Import