pub theorem ifpos (p: wff) (a b: nat): $ p -> if p a b = a $;
p -> (ifp p (n = a) (n = b) <-> n = a)
p -> the {n | ifp p (n = a) (n = b)} = a
p -> if p a b = a