thus <:F,G:> is Functor of A,[:B,C:] ; :: thesis: verum