Right. Put differently, we have that FPSan() is a well-defined function, so [ f = g ] => [ FPSan(f) = FPSan(g)], but we need to show that FPSan() is injective, i.e., [ FPSan(f) = FPSan(g) ] => [ f = g ]. I confess I haven't looked very closely but it should not be so hard. We can prove injectibility in the alternative by analyzing ker(FPSan()), the set of all inputs in the domain of functions mapping to the identity element in the co-domain. If the kernel is trivial and only consists of the identity map, the injectibility is established, but I am not immediately seeing the proof. Fun!