Coq formalization of "A Decision Procedure for Regular Expression Equivalence in Type Theory" by Coquand and Siles [maintainer=@anton-trunov]