src/ZF/Coind/ECR.thy

           <te,e_fn(x,e),t>:ElabRel;  
           ve_dom(ve) = te_dom(te);   
           {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
       |] ==>   
       <v_clos(x,e,ve),t>:HasTyRel" 
-  monos "[Pow_mono]"
+  monos  Pow_mono
   type_intrs "Val_ValEnv.intrs"
   
 (* Pointwise extension to environments *)
  
 consts