Object: type_inj_wf_for_quot, theory quot_1
Display form: 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])
Term structure: all(universe; T.all(function(T; .function(T; .prop)); E.implies(equiv_rel(T; x,y.so_apply(E; x; y)); all(T; a.member(quotient(T; x,y.so_apply(E; x; y)); type_inj(a; quotient(T; x,y.so_apply(E; x; y))))))))