First, we will construct a mapping $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_-$ which takes a closed type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau$ and produces a relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } {\sim_\tau} \subseteq \tau^2$

Then we conclude with the statement of the theorem, that for a value $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x$ of closed type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau$ we have that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x \sim_\tau x$.

For a type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau \in \Sigma$, we have that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_\tau$ relates values which are equal

Hence, for $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x : \tau \in \Sigma$, we conclude that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x \sim_\tau x$, meaning that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x = x$

The relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_{\tau \times \sigma}$ on the type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau \times \sigma$ relates values $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } (a, b)$ and $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } (x, y)$ iff $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } a \sim_\tau x$ and $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } b \sim_\tau y$.

So far we’ve only seen $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim$ meaning equality, and in that case $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim$ on product types just lifts equality to two-tuples. However, we are not guaranteed that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim$ is equality!

The relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_{\tau^\star}$ on the type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau^\star$ of lists over $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau$ relates two lists $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \bar x, \bar y : \tau^\star$ iff they are of the same length and respective elements are related

Again, the structure of this is akin to list equality, but just for an arbitrary relation

The relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_{\tau \to \sigma}$ on the type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \tau \to \sigma$ relates two functions $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } f, g : (\tau \to \sigma)$ if and only if for all $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x : \tau$ we have that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x \sim_\tau x'$ implies $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } f(x) \sim_\sigma g(x')$.

Once, again, this is kinda like a generalized equality lift.

The relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_{\forall \tau\ \rho(\tau)}$ on the type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \forall \tau\ \rho(\tau)$ relates two values $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x, y : \forall \tau\ \rho(\tau)$ if and only if for every type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sigma$ and relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \equiv$ over $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \rho(\sigma)$ we have that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x_\sigma \equiv y_\sigma$ Note: the syntax $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x_\sigma$ means the instantation of polymorphic value $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x$ at type $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sigma$

Now it gets interesting. Note that we did not stipulate that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \equiv$ need be $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sim_{\rho(\sigma)}$! It can be any relation over $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \sigma$ and we are still guaranteed that the instantiations $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } x_\sigma$ and $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } y_\sigma$ are related. We have then the guarantee that for any value $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } v : \forall \tau\ \rho(\tau)$ and relation $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \equiv$ over $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \rho(\sigma)$ that $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } v_\sigma \equiv v_\sigma$. (that... can’t be right. What if $\newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } \renewcommand{\rm}[1]{ \mathrm{#1} } \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } \newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } \newcommand{\smag}[1]{ { \lvert {#1} \rvert } } \newcommand{\card}{ \t{cd} } \newcommand{\dcup}{ \sqcup } \newcommand{\tup}[1]{ \langle {#1} \rangle } \newcommand{\tl}{ \tilde } \newcommand{\wt}{ \widetilde } \newcommand{\To}{ \Rightarrow } \newcommand{\box}[1]{ \fbox{$ #1 $} } \newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } } \newcommand{\tpar}[1]{ \left( {#1} \right) } \newcommand{\tbrak}[1]{ \left[ {#1} \right] } \newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } \newcommand{\mapsfrom}{ \mathrel{↤} } \newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\pre}[1]{{ \small `{#1} }} \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \newcommand{\id}{ \,\mathrm d } \newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } \newcommand{\dd}{ \ddn{} } \newcommand{\d}{ \dd{} } \newcommand{\dn}[1]{ \ddn{#1}{} } \newcommand{\Dn}[2]{ \partial^{#1}_{#2} } \newcommand{\D}{ \Dn{} } \newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } \newcommand{\cat}[1]{{ \sf{#1} }} \newcommand{\yo}{よ} \newcommand{\X}{-\!\!\!-\!\!\!} \newcommand{\xlongrightarrow}{ \mathop{ \, \X\longrightarrow \, } } \newcommand{\xxlongrightarrow}{ \mathop{ \, \X\X\longrightarrow \, } } \newcommand{\xxxlongrightarrow}{ \mathop{ \, \X\X\X\longrightarrow \, } } \newcommand{\takenby}[1]{ \overset{#1}{\rightarrow} } \newcommand{\longtakenby}[1]{ \overset{#1}{\longrightarrow} } \newcommand{\xlongtakenby}[1]{ \overset{#1}{\xlongrightarrow} } \newcommand{\xxlongtakenby}[1]{ \overset{#1}{\xxlongrightarrow} } \newcommand{\xxxlongtakenby}[1]{ \overset{#1}{\xxxlongrightarrow} } \newcommand{\apar}{ {-} } \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } \equiv$ is the empty relation?)