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