Coq proof of equivalence of micro and macro step semantics of cgals -- including data!