no more admit in groupoid_interpretation.v