Object: all_quot_elim, theory quot_1
Display form: 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])))
Term structure: all(universe; T.all(function(T; .function(T; .prop)); E.implies(equiv_rel(T; x,y.so_apply(E; x; y)); all(function(quotient(T; x,y.so_apply(E; x; y)); .prop); F.implies(all(quotient(T; x,y.so_apply(E; x; y)); w.sq_stable(apply(F; w))); iff(all(quotient(T; x,y.so_apply(E; x; y)); z.so_apply(F; z)); all(T; z.so_apply(F; z))))))))