The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

Dear Mark,

>[...] there is also Lem (https://github.com/rems-project/lem)
>which follows the same idea of exporting to multiple backends
>including multiple theorem provers (Isabelle/HOL, HOL4 and Coq).

Rodin Aarssen translated for his master thesis Robbert's
operational semantics of C to Lem, and then discovered that
in Lem one does not have the distinction between Prop and
bool.  As Robbert's semantics both contains if-then-else's
which need bool, as well as inductively defined predicates
which need Prop, this was a problem.

At least, that was the case when Rodin's thesis was written,
in 2016.  Things might be different now.

Freek