[cmrx64]

the binary expansion of 7 has three elements (you will find them at indexes Fin 0, Fin 1, and Fin 2) and the proof is of their equality.

[alimw]

The proof is actually of their equivalence as propositions. This is only possible because the binary digits are represented as Bools, and a Bool b can be coerced to the proposition that b = true.