(* The source calculus. *) module S = Tail (* The target calculus. *) module T = Top let defun_term (t : S.term) : T.program = assert false