[isabelle] Proof help on Cardinality and list_all2


I have been trying to see if there is a straightforward way to prove the 
following in Isabelle:

  card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x s}

Specifically, I suspect that this must have come up somewhere before, and 
I seet some statements that might be related in the various built-in 
theories, but I am so new to Isabelle that I am having trouble putting 
them together into a simple proof. I would appreciate any help on the 
nicest way to go about this proof. 

Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.

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