Object: dec_iff_ex_bvfun, theory quot_1
Display form: T:. E:T T . (x,y:T. Dec(E[x;y])) (f:T T . x,y:T. (x f y) E[x;y])
Term structure: all(universe; T.all(function(T; .function(T; .prop)); E.iff(all(T; x.all(T; y.decidable(so_apply(E; x; y)))); exists(function(T; .function(T; .bool)); f.all(T; x.all(T; y.iff(assert(infix_ap(f; x; y)); so_apply(E; x; y))))))))