Proof of iff_preserves_decidability