« Species on FinSet and action types

Lemma. [00DB]

isFinSet(X) is a proposition and equivalent to . See symmetry book lemma 2.24.4

Backlinks

Lemma. [00DE]

By Lemma 2.24.4 we get that