E:(
Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y)) 
(
h:(). (n,k:. (n E k) 
h(n) = h(k)) & (n:. n E (h(n))))
comp_choice
Thm* E:(Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y))
(h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n))))
comp_choice
Thm* E:(
), n,k:.
(EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk })
min_el_iff
Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn })
min_el_sound
Thm* E:(), n,k:.
(EquivRel x,y:. x E y) (n E k) Min{ x | xEn } = Min{ x | xEk }
min_el_unique
Thm* E:(TT), s,t:T. (EquivRel x,y:T. x E y) (s E t) E(s) = E(t)
equiv_rel_fun
In prior sections: rel 1