/coq/ex/test-cases/retract-completely-asserted/