inhabited: ∀i. i ∈ indexes → class i ≬ class i;
disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i = j;
covers: big_union support ? indexes (λx.class x) = full_set A
inhabited: ∀i. i ∈ indexes → class i ≬ class i;
disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i = j;
covers: big_union support ? indexes (λx.class x) = full_set A