const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f axiom bij_comp: !x:set.!y:set.!z:set.!f:set set.!f2:set set.bij x y f -> bij y z f2 -> bij x z \w:set.f2 (f w) claim !x:set.!y:set.!z:set.equip x y -> equip y z -> ?f:set set.bij x z f