[isabelle] Quantifier over empty set



Hi,

how can i write and prove:

"A = ∅ ⟹ (∀c∈dom A. B) = B "

Thanks
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.