On 07.05.2012 20:06, Aaron W. Hsu wrote:
show ?thesis by (simp add: eq_cart card_image subset_inj_on[OF inj] card_cartesian_product) qedWhat is the OF here? I understand the other elements, but what does the subset_inj_on[OF inj] part do?
A[OF B] discharges the first premise of A with B. -- Lars