Alessi, F.; Ciaffaglione, A.; Di Gianantonio, P.; Honsell, F.; Lenisa, M.; Scagnetto, I. LF+ in Coq for "fast and loose" Reasoning. JFR 2019, 12, 11-51.