:: deftheorem defines GRZ-ConjElimR GRZLOG_1:def 27 :
GRZ-ConjElimR = { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;