theorem Ifid (A: set) (p: wff): $ If p A A == A $;
p -> If p A A == A
~p -> If p A A == A
If p A A == A