467   shows "Bex R Q"

   467   shows "Bex R Q"

   468   using a b by (metis COMBC_def Collect_def Collect_mem_eq)

   468   using a b by (metis COMBC_def Collect_def Collect_mem_eq)

   469 

   469 

   470 lemma LEFT_RES_FORALL_REGULAR:

   470 lemma LEFT_RES_FORALL_REGULAR:

   471   assumes a: "!x. (R x \<and> (Q x --> P x))"

   471   assumes a: "!x. (R x \<and> (Q x --> P x))"

   473   using a

   473   using a

   474   apply (metis COMBC_def Collect_def Collect_mem_eq a)

   474   apply (metis COMBC_def Collect_def Collect_mem_eq a)

   475   done

   475   done

   476 

   476 

   477 lemma RIGHT_RES_FORALL_REGULAR:

   477 lemma RIGHT_RES_FORALL_REGULAR: