Object: decidable__quotient_equal, theory quot_1
Display form: 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))
Term structure: all(universe; T.all(function(T; .function(T; .prop)); E.implies(equiv_rel(T; x,y.so_apply(E; x; y)); implies(all(T; x.all(T; y.decidable(so_apply(E; x; y)))); all(quotient(T; x,y.so_apply(E; x; y)); u.all(quotient(T; x,y.so_apply(E; x; y)); v.decidable(equal(quotient(T; x,y.so_apply(E; x; y)); u; v))))))))