pub fn emit_rocq(source: &Program) -> Result<Emitted>
Emits a checked program as Rocq.
On constructs the target cannot express faithfully.