started on formalising specialisation

Convincing coq that specialisation is terminating is still a problem.