Definition cf := fun t0 t1 t2 : Type
   => fun (f : t1 -> t2) (g : t0 -> t1) => fun x => f (g x).
 Implicit Arguments cf [t0 t1 t2].
 Notation "f @ g" := (cf f g) (at level 65, left associativity).
 
 Definition cf_assoc := fun (t0 t1 t2 t3 : Type)
   (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1)
   => (refl_equal _) : (f @ g) @ h = f @ (g @ h).