# Re: [isabelle] Proof help on Cardinality and list_all2

Probably nothing exactly like this has come up before. There is a relevant fact, list_all2_Cons2, which you can find by searching for "list_all2 _ _ (_ # _)" with the find_theorems facility.
```
```
I can prove your equality by showing your set construction analogous to a cartesian product.
```
lemma
"card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x s}"
proof -
have eq_cart: "{x. list_all2 op < x (a # s)}
= (%(x, y). x # y) ` ({..< a} <*> {x. list_all2 op < x s})"
by (auto simp: list_all2_Cons2)
have inj: "inj (%(x, y). x # y)"
by (auto intro: inj_onI)
show ?thesis
by (simp add: eq_cart card_image subset_inj_on[OF inj]
card_cartesian_product)
qed

I wonder if there is a simpler proof.

```
Constructing terms using simple operators like image (`) and cartesian product (<*>) tends to make life easier in Isabelle, since it is clear what combinations of operators to search for rules about. Searching for "card (_ <*> _)" locates card_cartesian_product and "card (_ ` _)" yields card_image, etc.
```
Yours,
Thomas.

On 07/05/12 12:22, Aaron W. Hsu wrote:
```
```Hello:

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
```