1 open Rec;
2
3 goalw thy [mono_def,Domf_def] "mono(Domf(F))";
4 by (DEPTH_SOLVE (slow_step_tac set_cs 1));
5 qed "mono_Domf";