Variable L : Type.
Variable betas : L -> L -> Prop.

Definition normal t : Prop := (* le terme t est en forme normale *)

.

Definition confluent : Prop := (* la relation betas est confluente *)

.

Definition has_normal  t : Prop := (* le terme t admet une forme normale *)

.

Check (* propriété il existe des termes qui n'ont pas de forme normale *)

.