import homotopy.circle
open circle

attribute circle.elim_on [recursor 2]

print [recursor] circle.elim_on