<div dir="ltr">The contruct function uses catchall.<br><div><br><a href="https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLL.agda#L604">https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLL.agda#L604</a><br><br></div><div>Then have a look at the function that proves a property that uses contruct at its type:<br><br><a href="https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLLProp.agda#L1442">https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLLProp.agda#L1442</a><br></div></div>