const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f axiom bij_id: !x:set.bij x x \y:set.y claim !x:set.?f:set set.bij x x f