let FOO = thm `;
    thus T;
  `;;