I mean, consider a trick like replacing axioms {A, B} with {A or B, A implies B, B implies A}. Of course it’s what you call an “obvious substitution”: it requires only a small amount of Boolean reasoning. But showing that NOR and NAND can express each other also requires only a small amount of Boolean reasoning! To my intuition there doesn’t seem any clear line between these cases.
I mean, consider a trick like replacing axioms {A, B} with {A or B, A implies B, B implies A}. Of course it’s what you call an “obvious substitution”: it requires only a small amount of Boolean reasoning. But showing that NOR and NAND can express each other also requires only a small amount of Boolean reasoning! To my intuition there doesn’t seem any clear line between these cases.