Introduce type for Subset

Essentially a Sigma type with irrelevant proof
Lemma 2.4 : Complete proof of class B