Revision 83e8e74005a9114cb71b1b01d1c309ba92a0f0ae

@CoqExtraction/Letouzey/2/2.1

#The difficulties in the removal of logical parts