Move part of formal proof to the implementation