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

Definition normal t : Prop := 
  forall u, betas t u -> t=u.

Definition confluent : Prop := 
  forall t u v, betas t u -> betas t v 
  -> exists w, betas u w /\ betas v w.

Definition has_normal  t : Prop := 
   exists u, betas t u /\ normal u.

Check exists t, forall u, betas t u -> ~ normal u.