reconsider a = a, b = b as Element of Funcs Y,BOOLEAN ;
a 'eqv' b is Element of Funcs Y,BOOLEAN ;
hence a 'eqv' b is Element of Funcs Y,BOOLEAN ; :: thesis: verum