After an experiment, the weight is being shifted onto Isabelle/HOL. See https://github.com/pirapira/eth-isabelle
coq