COM	quot_1_begin	************ QUOT_1 ************
COM	quot_1_summary	Support lemmas for quotient type.
COM	quot_1_intro	Basic support for quotient type.
THM	quotient_wf	T:. E:T T . EquivRel(T;x,y.E[x;y]) x,y:T//E[x;y]
THM	quotient_qinc	T:. E:T T . EquivRel(T;x,y.E[x;y]) T x,y:T//E[x;y]
THM	type_inj_wf_for_quot	T:. E:T T . EquivRel(T;x,y.E[x;y]) (a:T. [a]{x,y:T//E[x;y]} x,y:T//E[x;y])
THM	quot_elim	T:. E:T T . EquivRel(T;x,y.E[x;y]) (a,b:T. a = b E[a;b])
THM	all_quot_elim	T:. E:T T . EquivRel(T;x,y.E[x;y]) (F:x,y:T//E[x;y] (w:x,y:T//E[x;y]. SqStable(F w)) ((z:x,y:T//E[x;y]. F[z]) (z:T. F[z])))
THM	dec_iff_ex_bvfun	T:. E:T T . (x,y:T. Dec(E[x;y])) (f:T T . x,y:T. (x f y) E[x;y])
THM	decidable__quotient_equal	T:. E:T T . EquivRel(T;x,y.E[x;y]) (x,y:T. Dec(E[x;y])) (u,v:x,y:T//E[x;y]. Dec(u = v))
COM	quot_1_end	********************************