idempotent -> involutive (+ remove gradLemma_old)
fixing spector lemma
merge guillaume in heterogeneous
delete trailing whitespaces in nIso