Proved that infer_top_side always holds

Still requires 3 cheats where bad side conditions are generated by the
translator.