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