Someone

     ( x : a                                                         !    
     !                                                               !    
     ! g : all y : a => b y                                          !    
     !                                                               !    
     ! f : all y : b x => c y ;  a : * ;  b : a -> * ;  c : b x -> * !    
let  !---------------------------------------------------------------! ;  
     !                    compose f g x : c (g x)                    )