@CoqExtraction/Letouzey/2/2.1

#The difficulties in the removal of logical parts