Goal:
    x : t  X : lt x x
  ============================
   False


DEBUG:Going to execute:
DepElim.is_introduced H; CoreTactics.block_goal;
            CoreTactics.revert_until H; CoreTactics.block_goal