const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f const inv : set (set set) set set axiom bij_inv: !x:set.!y:set.!f:set set.bij x y f -> bij y x (inv x f) claim !x:set.!y:set.equip x y -> ?f:set set.bij y x f