gdc-gbi-in-coq