qualif Snd( v : b_t, 
            p : Pred  b_t  a, 
            a : fix##40##41#  a  b): 
          (papp2 p v (fst a))

qualif Fst( v : a, 
            a : fix##40##41#  a  b): 
           (v = fst a)