Normalization by Evaluation with Substitutions as Operations

By case analysis on the argument:

By induction on t. We show a few representative cases.

t = x (variable).

\begin{aligned} x[\ensuremath{\textsf{id}}] = \ensuremath{\textsf{id}}(x) = x \end{aligned}

t = \lambda x.\, t'.

\begin{aligned} (\lambda x.\, t')[\ensuremath{\textsf{id}}] &= \lambda x.\, (t'[q(\ensuremath{\textsf{id}})]) \\ &= \lambda x.\, (t'[\ensuremath{\textsf{id}}]) \tag{by \Cref{lem:wk-q-id}} \\ &= \lambda x.\, t' \end{aligned}

t = \Pi(x : S).\, T.

\begin{aligned} (\Pi(x : S).\, T)[\ensuremath{\textsf{id}}] &= \Pi(x : S[\ensuremath{\textsf{id}}]).\, (T[q(\ensuremath{\textsf{id}})]) \\ &= \Pi(x : S).\, (T[\ensuremath{\textsf{id}}]) \tag{by IH and \Cref{lem:wk-q-id}} \\ &= \Pi(x : S).\, T \end{aligned}

All other cases follow the same pattern.

By case analysis on the argument:

By induction on t. We show a few representative cases.

t = x (variable).

\begin{aligned} x[\phi][\psi] = (\phi(x))[\psi] = \psi(\phi(x)) = (\phi \circ \psi)(x) = x[\phi \circ \psi] \end{aligned}

t = \lambda x.\, t'.

\begin{aligned} (\lambda x.\, t')[\phi][\psi] &= (\lambda x.\, (t'[q(\phi)]))[\psi] \\ &= \lambda x.\, (t'[q(\phi)][q(\psi)]) \\ &= \lambda x.\, (t'[q(\phi) \circ q(\psi)]) \\ &= \lambda x.\, (t'[q(\phi \circ \psi)]) \tag{by \Cref{lem:wk-q-comp}} \\ &= (\lambda x.\, t')[\phi \circ \psi] \end{aligned}

t = \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x, y.\, s)~t'}.

\begin{aligned} & (\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x, y.\, s)~t'})[\phi][\psi] \\ &= (\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\phi)])~z[\phi]~(x, y.\, s[q^2(\phi)])~t'[\phi]})[\psi] \\ &= \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\phi)][q(\psi)])~z[\phi][\psi]~(x, y.\, s[q^2(\phi)][q^2(\psi)])~t'[\phi][\psi]} \\ &= \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\phi) \circ q(\psi)])~z[\phi \circ \psi]~(x, y.\, s[q^2(\phi) \circ q^2(\psi)])~t'[\phi \circ \psi]} \\ &= \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\phi \circ \psi)])~z[\phi \circ \psi]~(x, y.\, s[q^2(\phi \circ \psi)])~t'[\phi \circ \psi]} \tag{by \Cref{lem:wk-qn-comp}} \\ &= (\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x, y.\, s)~t'})[\phi \circ \psi] \end{aligned}

The cases for \textsf{succ}~t, r\; s, \Pi, \ensuremath{\texttt{Nat}}, \ensuremath{\texttt{Ty}_{i}}, and \textsf{zero} are similar or immediate.

All three are immediate from the definition of composition as function composition on \mathbb{N}:

By induction on t. The key observation is that q(\iota(\phi)) = \iota(q(\phi)):

With this fact, the induction is straightforward: at each binding form, we use q(\iota(\phi)) = \iota(q(\phi)) to relate the substitution side to the weakening side. For example:

\iota(\ensuremath{\textsf{id}})(x) = \ensuremath{\textsf{id}}(x) = x = \ensuremath{\textsf{id}}(x). \iota(\Uparrow)(x) = \Uparrow(x) = x + 1. As a substitution, this is the variable x+1, which equals \Uparrow viewed as a substitution. Already shown in the proof of ?: q(\iota(\phi))(0) = 0 = \iota(q(\phi))(0) and q(\iota(\phi))(x+1) = \phi(x) + 1 = \iota(q(\phi))(x+1). We verify pointwise:

\begin{aligned} (\iota(\phi) \circ \iota(\psi))(x) &= \iota(\phi)(x)[\iota(\psi)] \\ &= \phi(x)[\iota(\psi)] \\ &= \psi(\phi(x)) \tag{by \Cref{lem:wk-embed-correct}} \\ &= (\phi \circ \psi)(x) \\ &= \iota(\phi \circ \psi)(x) \end{aligned}

By case analysis:

By induction on t.

t = x (variable). x[\ensuremath{\textsf{id}}] = \ensuremath{\textsf{id}}(x) = x. t = \lambda x.\, t'.

\begin{aligned} (\lambda x.\, t')[\ensuremath{\textsf{id}}] &= \lambda x.\, (t'[q(\ensuremath{\textsf{id}})]) \\ &= \lambda x.\, (t'[\ensuremath{\textsf{id}}]) \tag{by \Cref{lem:subst-q-id}} \\ &= \lambda x.\, t' \end{aligned}

t = \Pi(x:S).\, T.

\begin{aligned} (\Pi(x:S).\, T)[\ensuremath{\textsf{id}}] &= \Pi(x : S[\ensuremath{\textsf{id}}]).\, (T[q(\ensuremath{\textsf{id}})]) \\ &= \Pi(x : S).\, (T[\ensuremath{\textsf{id}}]) \tag{by IH and \Cref{lem:subst-q-id}} \\ &= \Pi(x : S).\, T \end{aligned}

All other cases are similar.

By induction on n.

n = 0: (1) vacuous. (2) q^0(\phi)(0) = \phi(0) = \phi(0) + 0. (3) q^0(\phi)(x) = \phi(x) = \phi(x - 0) + 0. n + 1: We use q^{n+1}(\phi) = q(q^n(\phi)).

If x < n+1: either x = 0 (then q(q^n(\phi))(0) = 0 = x) or x = y + 1 with y < n (then q(q^n(\phi))(y+1) = q^n(\phi)(y) + 1 = y + 1 = x by the IH). x = n + 1: q(q^n(\phi))(n+1) = q^n(\phi)(n) + 1 = (\phi(0) + n) + 1 = \phi(0) + (n+1) by the IH. x > n + 1: x = y + 1 with y > n. q(q^n(\phi))(y+1) = q^n(\phi)(y) + 1 = (\phi(y - n) + n) + 1 = \phi((y+1) - (n+1)) + (n+1) by the IH.

By induction on n.

n = 0: (1) vacuous. (2) q^0(\sigma)(0) = \sigma(0) = \sigma(0)[\Uparrow^0]. (3) q^0(\sigma)(x) = \sigma(x) = \sigma(x-0)[\Uparrow^0]. n + 1: We use q^{n+1}(\sigma) = q(q^n(\sigma)).

If x < n+1: either x = 0 (then q(q^n(\sigma))(0) = 0 = x) or x = y + 1 with y < n (then q(q^n(\sigma))(y+1) = (q^n(\sigma)(y))[\Uparrow] = y[\Uparrow] = y + 1 = x by the IH (1)). x = n + 1:

\begin{aligned} q(q^n(\sigma))(n+1) &= (q^n(\sigma)(n))[\Uparrow] \\ &= (\sigma(0)[\Uparrow^n])[\Uparrow] \\ &= \sigma(0)[\Uparrow^{n+1}] \tag{by \Cref{lem:wk-comp}} \end{aligned}

x > n+1: x = y + 1 with y > n.

\begin{aligned} q(q^n(\sigma))(y+1) &= (q^n(\sigma)(y))[\Uparrow] \\ &= (\sigma(y - n)[\Uparrow^n])[\Uparrow] \\ &= \sigma(y - n)[\Uparrow^{n+1}] \tag{by \Cref{lem:wk-comp}} \\ &= \sigma((y+1) - (n+1))[\Uparrow^{n+1}] \end{aligned}

By case analysis:

At index 0:

\begin{aligned} (q(\sigma) \circ q(\tau))(0) = q(\sigma)(0)[q(\tau)] = 0[q(\tau)] = q(\tau)(0) = 0 = q(\sigma \circ \tau)(0) \end{aligned}

At index x+1:

\begin{aligned} (q(\sigma) \circ q(\tau))(x+1) &= (q(\sigma)(x+1))[q(\tau)] \\ &= (\sigma(x))[\Uparrow][q(\tau)] \\ &= (\sigma(x))[\tau][\Uparrow] \tag{by \Cref{lem:wk-subst-comm}} \\ &= ((\sigma \circ \tau)(x))[\Uparrow] \\ &= q(\sigma \circ \tau)(x+1) \end{aligned}

By induction on t.

t = x (variable). x[\sigma][\tau] = \sigma(x)[\tau] = (\sigma \circ \tau)(x) = x[\sigma \circ \tau]. t = \lambda x.\, t'.

\begin{aligned} (\lambda x.\, t')[\sigma][\tau] &= (\lambda x.\, t'[q(\sigma)])[\tau] \\ &= \lambda x.\, (t'[q(\sigma)][q(\tau)]) \\ &= \lambda x.\, (t'[q(\sigma) \circ q(\tau)]) \\ &= \lambda x.\, (t'[q(\sigma \circ \tau)]) \tag{by \Cref{lem:subst-q-comp}} \\ &= (\lambda x.\, t')[\sigma \circ \tau] \end{aligned}

t = \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x,y.\,s)~t'}.

\begin{aligned} &(\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x,y.\,s)~t'})[\sigma][\tau] \\ &= (\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\sigma)])~z[\sigma]~(x,y.\,s[q^2(\sigma)])~t'[\sigma]})[\tau] \\ &= \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\sigma)][q(\tau)])~z[\sigma][\tau]~(x,y.\,s[q^2(\sigma)][q^2(\tau)])~t'[\sigma][\tau]} \\ &= \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T[q(\sigma \circ \tau)])~z[\sigma \circ \tau]~(x,y.\,s[q^2(\sigma \circ \tau)])~t'[\sigma \circ \tau]} \tag{by IH and \Cref{lem:subst-q-comp}} \\ &= (\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x,y.\,s)~t'})[\sigma \circ \tau] \end{aligned}

Other cases are similar.

Since \sigma[\phi] = \sigma \circ \phi (treating \phi as a substitution), we have:

Statement (1) is a corollary of ?, ?. Since we elide the embedding, treating \phi as a substitution:

Statement (2) also follows from ?:

We verify: (\sigma \circ \phi)(x) = \sigma(x)[\phi] = (\sigma[\phi])(x), which is exactly the definition of \sigma[\phi]. Hence \sigma \circ \phi = \sigma[\phi] and the claim holds.

Pointwise:

Pointwise:

By ?, it suffices to show q(\sigma) \circ (\ensuremath{\textsf{id}}, s/x) = (\sigma, s/x). Recall q(\sigma) = (\sigma[\Uparrow], 0/x). By ?:

By ?, it suffices to show q(\sigma) \circ (\phi, s/x) = (\sigma[\phi], s/x). Recall q(\sigma) = (\sigma[\Uparrow], 0/x).

(\ensuremath{\textsf{id}} \circ \sigma)(x) = \ensuremath{\textsf{id}}(x)[\sigma] = x[\sigma] = \sigma(x). (\sigma \circ \ensuremath{\textsf{id}})(n) = \sigma(x)[\ensuremath{\textsf{id}}] = \sigma(x) by ?. By pointwise calculation:

\begin{aligned} ((\sigma \circ \tau) \circ \delta)(x) &= ((\sigma \circ \tau)(x))[\delta] \\ &= (\sigma(x)[\tau])[\delta] \\ &= \sigma(x)[\tau \circ \delta] \tag{by \Cref{lem:subst-assoc}} \\ &= (\sigma \circ (\tau \circ \delta))(x) \end{aligned}

We show both sides equal t[\sigma, s[\sigma]/x].

Pointwise:

Hence both sides agree at every index.

We must show: for all x : T \in \Gamma, \ensuremath{\textsf{id}}(x) : T[\ensuremath{\textsf{id}}] \in \Gamma. Since \ensuremath{\textsf{id}}(x) = x and T[\ensuremath{\textsf{id}}] = T (by ?), this is immediate from x : T \in \Gamma.

We must show: for all y : T \in \Gamma, \Uparrow(y) : T[\Uparrow] \in \Gamma, x_0 : S. We have \Uparrow(y) = 1 + y. From y : T \in \Gamma, the lookup rule gives 1{+}y : T[\Uparrow] \in \Gamma, x_0 : S.

We must show: for all y : T \in \Delta, x_0 : S, q(\phi)(y) : T[q(\phi)] \in \Gamma, x_0 : S[\phi]. We case-split on the lookup y : T \in \Delta, x_0 : S:

x_0 : S[\Uparrow] \in \Delta, x_0 : S: Then q(\phi)(x_0) = x_0 and S[\Uparrow][q(\phi)] = S[\phi][\Uparrow] (by ?). We have x_0 : S[\phi][\Uparrow] \in \Gamma, x_0 : S[\phi] by lookup. 1{+}z : T'[\Uparrow] \in \Delta, x_0 : S where z : T' \in \Delta: Then q(\phi)(1{+}z) = 1{+}\phi(z) and T'[\Uparrow][q(\phi)] = T'[\phi][\Uparrow] (by ?). From \wkjudge[\phi]{\Delta : , we have \phi(z) : T'[\phi] \in \Gamma, so 1{+}\phi(z) : T'[\phi][\Uparrow] \in \Gamma, x_0 : S[\phi] by lookup.

We must show: for all x : T \in \Theta, (\phi \circ \psi)(x) : T[\phi \circ \psi] \in \Gamma.

Hence (\phi \circ \psi)(x) : T[\phi \circ \psi] \in \Gamma.

By mutual induction on the derivation of the syntactic judgment. We show representative cases for statement (1).

Case

Then y[\phi] = \phi(y). By the definition of \weakening[\Delta] \phi \Gamma, \phi(y) : T[\phi] \in \Delta. By Var, \typing[\Delta]{\phi(y)}{T[\phi]}.

Case

We must show \typing[\Delta]{(\lambda y.\,t)[\phi]}{(\Pi(y:S').\,T)[\phi]}, i.e. \typing[\Delta]{\lambda y.\,(t[q(\phi)])}{\Pi(y:S'[\phi]).\,(T[q(\phi)])}.

Case

It remains to show T[q(\phi)][s[\phi]/y] = T[s/y][\phi], which is ?.

Case

We now show representative cases for statement (2).

Case

We must show \tyequiv[\Delta]{((\lambda x.\,t)\;s)[\phi]}{t[s/x][\phi]}{T'[s/x][\phi]}.

Now:

By ?: t[q(\phi)][s[\phi]/x] = t[s/x][\phi] and T'[q(\phi)][s[\phi]/x] = T'[s/x][\phi].

Case

We must show \tyequiv[\Delta]{t[\phi]}{(\lambda x.\,(t[\Uparrow]\;x))[\phi]}{(\Pi(x:S').\,T')[\phi]}. Unfolding the right-hand side:

We show a case for statement (3).

Case

This is \subty[\Delta]{(\Pi(x:S).\,T)[\phi]}{(\Pi(x:S').\,T')[\phi]}.

The remaining cases (U-Wf, N-Wf, \Pi-Wf, Ze-I, Su-I, N-E, congruence rules, Sub-Univ, Sub-Trans, Sub-Eq) are analogous: apply the IH to each premise, using ? to construct the weakening for extended contexts, and re-apply the rule.

We must show: for all x : T \in \Gamma, \typing[\Gamma]{\ensuremath{\textsf{id}}(x)}{T[\ensuremath{\textsf{id}}]}. Since \ensuremath{\textsf{id}}(x) = x and T[\ensuremath{\textsf{id}}] = T (by ?), this reduces to \typing[\Gamma]{x}{T}, which holds by Var.

We must show: for all y : T \in \Delta, x : S, \typing[\Gamma]{(\sigma, s/x)(y)}{T[(\sigma, s/x)]}.

x_0 : S[\Uparrow] \in \Delta, x : S: Then (\sigma, s/x)(x_0) = s and S[\Uparrow][(\sigma, s/x)] = S[\sigma] (by ?, ?). We have \typing[\Gamma]{s}{S[\sigma]} by assumption. 1{+}z : T'[\Uparrow] \in \Delta, x : S with z : T' \in \Delta: Then (\sigma, s/x)(1{+}z) = \sigma(z) and T'[\Uparrow][(\sigma, s/x)] = T'[\sigma] (by ?, ?). From \judge[\Gamma]{\sigma : \Delta}, \typing[\Gamma]{\sigma(z)}{T'[\sigma]}.

By ? and ?: \ensuremath{\textsf{id}} is well-typed by ?, and \typing[\Gamma]{s}{S} = \typing[\Gamma]{s}{S[\ensuremath{\textsf{id}}]} by ?.

We must show: for all x : T \in \Delta, \typing[\Gamma']{(\sigma[\phi])(x)}{T[\sigma[\phi]]}. From \judge[\Gamma]{\sigma : \Delta}, \typing[\Gamma]{\sigma(x)}{T[\sigma]}. By ?, \typing[\Gamma']{\sigma(x)[\phi]}{T[\sigma][\phi]}. Now (\sigma[\phi])(x) = \sigma(x)[\phi] and T[\sigma[\phi]] = T[\sigma][\phi] (by ?).

We must show that q(\sigma) maps each variable in (\Delta, x_0 : S) to a well-typed term in (\Gamma, x_0 : S[\sigma]). We case-split on the lookup in (\Delta, x_0 : S):

x_0 : S[\Uparrow] \in \Delta, x_0 : S:

\begin{aligned} &q(\sigma)(x_0) = x_0 \\ &S[\Uparrow][q(\sigma)] = S[\sigma][\Uparrow] && \text{(by \Cref{lem:wk-subst-comm})} \\ &x_0 : S[\sigma][\Uparrow] \in \Gamma, x_0 : S[\sigma] && \text{(by lookup)} \end{aligned}

Hence \typing[\Gamma, x_0 : S[\sigma]]{x_0}{S[\Uparrow][q(\sigma)]} by Var. 1{+}y : T[\Uparrow] \in \Delta, x_0 : S where y : T \in \Delta:

\begin{aligned} &q(\sigma)(1{+}y) = \sigma(y)[\Uparrow] \\ &\typing[\Gamma]{\sigma(y)}{T[\sigma]} && \text{(from $\judge[\Gamma]{\sigma : \Delta}$)} \\ &\typing[\Gamma, x_0 : S[\sigma]]{\sigma(y)[\Uparrow]}{T[\sigma][\Uparrow]} && \text{(by \Cref{lem:wk-typing} using \Cref{lem:wk-shift-wt})} \\ &T[\Uparrow][q(\sigma)] = T[\sigma][\Uparrow] && \text{(by \Cref{lem:wk-subst-comm})} \end{aligned}

Hence \typing[\Gamma, x_0 : S[\sigma]]{\sigma(y)[\Uparrow]}{T[\Uparrow][q(\sigma)]}.

By mutual induction on the derivation of the syntactic judgment. We show representative cases for statement (1).

Case

Then t[\sigma] = x[\sigma] = \sigma(x). By the definition of \judge[\Gamma]{\sigma : \Delta}, we have \typing[\Gamma]{\sigma(x)}{T[\sigma]}, which is the goal.

Case

We must show \typing[\Gamma]{(\lambda x.\,t')[\sigma]}{(\Pi(x:S).\,T)[\sigma]}. Unfolding:

Now:

Case

We must show \typing[\Gamma]{(r\;s)[\sigma]}{(T[s/x])[\sigma]}. Unfolding: (r\;s)[\sigma] = r[\sigma]\;s[\sigma].

It remains to show T[q(\sigma)][s[\sigma]/x] = (T[s/x])[\sigma], which is ?.

Case

The remaining cases (U-Wf, N-Wf, Ze-I, Su-I) are straightforward applications of the IH.

We now show representative cases for statement (2). The congruence cases follow directly from the IH. We show the computation and uniqueness rules.

Case

We must show \tyequiv[\Gamma]{((\lambda x.\,t)\;s)[\sigma]}{t[s/x][\sigma]}{T[s/x][\sigma]}. Unfolding:

Now:

By ?: t[q(\sigma)][s[\sigma]/x] = (t[s/x])[\sigma] and T[q(\sigma)][s[\sigma]/x] = (T[s/x])[\sigma].

Case

We must show \tyequiv[\Gamma]{t[\sigma]}{(\lambda x.\,(t[\Uparrow]\;x))[\sigma]}{(\Pi(x:S).\,T)[\sigma]}. Unfolding the right-hand side:

Now:

We now show representative cases for statement (3).

Case

Then \ensuremath{\texttt{Ty}_{i}}[\sigma] = \ensuremath{\texttt{Ty}_{i}} and \ensuremath{\texttt{Ty}_{j}}[\sigma] = \ensuremath{\texttt{Ty}_{j}}. From \judge[\Gamma]{\sigma : \Delta}, we have \vdash \Gamma. By Sub-Univ, \IfNoValueTF {\ensuremath{\texttt{Ty}_{i}}} {\Gamma \vdash \ensuremath{\texttt{Ty}_{j}} \subseteq Ty_i Ty_j } . \medskip\noindent \textbf{Case} \begin{mathpar} \inferrule {\typing[\Delta]{S}{\ensuremath{\texttt{Ty}_{i}}} \\ \typing[\Delta]{S'}{\ensuremath{\texttt{Ty}_{i}}} \\ \tyequiv[\Delta]{S}{S'}{\ensuremath{\texttt{Ty}_{i}}} \\ \typing[\Delta, x:S]{T}{\ensuremath{\texttt{Ty}_{i}}} \\ \typing[\Delta, x:S']{T'}{\ensuremath{\texttt{Ty}_{i}}} \\ \subty[\Delta, x:S]{T}{T'}} {\subty[\Delta]{\Pi(x:S).\,T}{\Pi(x:S').\,T'}} \end{mathpar} \begin{align*} &\typing[\Gamma]{S[\sigma]}{\ensuremath{\texttt{Ty}_{i}}} && \text{(by IH)} \\ &\typing[\Gamma]{S'[\sigma]}{\ensuremath{\texttt{Ty}_{i}}} && \text{(by IH)} \\ &\tyequiv[\Gamma]{S[\sigma]}{S'[\sigma]}{\ensuremath{\texttt{Ty}_{i}}} && \text{(by IH, statement (2))} \\ &\typing[\Gamma, x:S[\sigma]]{T[q(\sigma)]}{\ensuremath{\texttt{Ty}_{i}}} && \text{(by IH using \Cref{lem:q-subst-typing})} \\ &\typing[\Gamma, x:S'[\sigma]]{T'[q(\sigma)]}{\ensuremath{\texttt{Ty}_{i}}} && \text{(by IH using \Cref{lem:q-subst-typing})} \\ &\subty[\Gamma, x:S[\sigma]]{T[q(\sigma)]}{T'[q(\sigma)]} && \text{(by IH, statement (3), using \Cref{lem:q-subst-typing})} \\ & \IfNoValueTF {\Pi(x:S[\sigma]).\,(T[q(\sigma)])} {\Gamma \vdash \Pi(x:S'[\sigma]).\,(T'[q(\sigma)]) \subseteq &} {\Pi(x:S[\sigma]).\,(T[q(\sigma)]) \vdash \Pi(x:S'[\sigma]).\,(T'[q(\sigma)]) \subseteq &} & \text{(by \textsc{Sub-Pi})} \end{align*} This is ((x:S). T)[] ((x:S’). T’)[] } {(\Pi(x:S).\,T)[\sigma] \vdash (\Pi(x:S').\,T')[\sigma] \subseteq .

Case Sub-Trans: By two applications of the IH and Sub-Trans.

Case Sub-Eq: By statement (2) and Sub-Eq.

We must show: for all x : T \in \Delta, \typing[\Gamma']{(\sigma \circ \tau)(x)}{T[\sigma \circ \tau]}.

By ? and ?, noting t[s/x] = t[\ensuremath{\textsf{id}}, s/x].

By mutual induction on the derivation.

Case

We have \vdash \Gamma immediately from the premise. For \typing[\Gamma]{T}{\ensuremath{\texttt{Ty}_{i}}}, we do induction on x : T \in \Gamma. If \Gamma = \Gamma', x : T, then \vdash \Gamma', x : T was derived by Ctx-Ext from \typing[\Gamma']{T}{\ensuremath{\texttt{Ty}_{i}}}; weakening gives \typing[\Gamma]{T}{\ensuremath{\texttt{Ty}_{i}}}. If \Gamma = \Gamma', y : S and x : T \in \Gamma', then by IH on the smaller context \typing[\Gamma']{T}{\ensuremath{\texttt{Ty}_{i}}}; weakening gives \typing[\Gamma]{T}{\ensuremath{\texttt{Ty}_{i}}}.

Case

We have \vdash \Gamma from the premise. The type of the conclusion is \ensuremath{\texttt{Ty}_{1+i}}, and \typing[\Gamma]{\ensuremath{\texttt{Ty}_{1+i}}}{\ensuremath{\texttt{Ty}_{2+i}}} by another application of U-Wf.

Case

Case

Case

Case

Case

Case

We have \vdash \Gamma from the premise. \typing[\Gamma]{x}{T} by Var. \typing[\Gamma]{T}{\ensuremath{\texttt{Ty}_{i}}} by the same argument as the Var typing case above.

Case

Case

Case

Case

Case

The remaining cases follow similar patterns.

By ?, \judge[\Gamma, x:S[\sigma]]{q(\sigma) : (\Delta, x:S)}. We need \judge[\Gamma, x:S[\sigma]]{q(\sigma') : (\Delta, x:S)} as well: from \tyequiv[\Gamma]{S[\sigma]}{S[\sigma']}{\ensuremath{\texttt{Ty}_{i}}} (by ? statement (2) applied to reflexivity on \typing[\Delta]{S}{\ensuremath{\texttt{Ty}_{i}}}), the contexts \Gamma, x:S[\sigma] and \Gamma, x:S[\sigma'] are equivalent, so \judge[\Gamma, x:S[\sigma]]{q(\sigma') : (\Delta, x:S)} by ? and a context-conversion step.

We verify clause (2): for every y : T \in \Delta, x:S, \tyequiv[\Gamma, x:S[\sigma]]{q(\sigma)(y)}{q(\sigma')(y)} {T[q(\sigma)]}.

y = x_0: T = S[\Uparrow], q(\sigma)(x_0) = x_0 = q(\sigma')(x_0). The required equality is reflexivity on x_0 at S[\Uparrow][q(\sigma)] = S[\sigma][\Uparrow] (by ?). y = 1{+}z where z : T' \in \Delta: q(\sigma)(1{+}z) = \sigma(z)[\Uparrow] and q(\sigma')(1{+}z) = \sigma'(z)[\Uparrow]. By clause (2) of ? on \sigma \approx \sigma', \tyequiv[\Gamma]{\sigma(z)}{\sigma'(z)}{T'[\sigma]}. By ? applied to \Uparrow, \tyequiv[\Gamma, x:S[\sigma]] {\sigma(z)[\Uparrow]}{\sigma'(z)[\Uparrow]} {T'[\sigma][\Uparrow]}, and T'[\sigma][\Uparrow] = T'[\Uparrow][q(\sigma)] by ?, which equals T[q(\sigma)].

By mutual induction on the syntactic derivation, parallel to ?. We show representative cases for statement (1).

Case

Then x[\sigma] = \sigma(x) and x[\sigma'] = \sigma'(x).

Case

We must show \tyequiv[\Gamma]{(\lambda x.\,t)[\sigma]}{(\lambda x.\,t)[\sigma']} {(\Pi(x:S).\,T)[\sigma]}. We first lift the equivalence under q:

Case

We must show \tyequiv[\Gamma]{(r\;s)[\sigma]}{(r\;s)[\sigma']}{T[s/x][\sigma]}.

Case

\ensuremath{\texttt{Ty}_{i}}[\sigma] = \ensuremath{\texttt{Ty}_{i}} and \ensuremath{\texttt{Ty}_{i}}[\sigma'] = \ensuremath{\texttt{Ty}_{i}}.

Case N-Wf: Analogous to U-Wf, with \ensuremath{\texttt{Nat}}[\sigma] = \ensuremath{\texttt{Nat}} = \ensuremath{\texttt{Nat}}[\sigma'] and reflexivity by N-Cong.

Case

Case Ze-I: \textsf{zero}[\sigma] = \textsf{zero} = \textsf{zero}[\sigma']; apply Ze-Cong. The type \ensuremath{\texttt{Nat}}[\sigma] = \ensuremath{\texttt{Nat}}.

Case

Case N-E: analogous to \lambda-E, applying the IH to each premise (motive, zero branch, step branch, scrutinee), lifting via q(\sigma) \approx q(\sigma') and q^2(\sigma) \approx q^2(\sigma'), and concluding by N-E-Cong.

Case

Statement (2): term-equality preservation. By induction on the term-equality derivation.

Case (Congruence rules: Var-Cong, U-Cong, N-Cong, \Pi-Cong, Ze-Cong, Su-Cong, \lambda-Cong, App-Cong, N-E-Cong). Each follows by IH on the premises and the same congruence rule, with substitution-on-syntax computed exactly as in statement (1).

Case

We must show \tyequiv[\Gamma]{((\lambda x.\,t)\;s)[\sigma]}{t[s/x][\sigma']} {T[s/x][\sigma]}.

By ? on \sigma \approx \sigma' at S: \judge[\Gamma, x:S[\sigma]]{q(\sigma) \approx q(\sigma') : (\Delta, x:S)}. Apply IH statement (1) to the third premise \typing[\Delta, x:S]{t}{T} and to the fourth premise \typing[\Delta]{s}{S}:

Build the head-extended substitution equivalence:

Apply IH statement (1) on the third premise \typing[\Delta, x:S]{t}{T} at this equivalence:

Case

We must show \tyequiv[\Gamma]{t[\sigma]}{(\lambda x.\,(t[\Uparrow]\;x))[\sigma']} {(\Pi(x:S).\,T)[\sigma]}.

By IH statement (1) on the third premise:

Apply ? statement (2) on the original \eta-rule at \sigma' (a well-typed substitution since \judge[\Gamma]{\sigma' : \Delta} by ? clause (1)):

Bridge the type from \sigma' to \sigma via the \Pi-Wf case of statement (1), already proved on \typing[\Delta]{\Pi(x:S).\,T}{\ensuremath{\texttt{Ty}_{i}}} (derivable from the first two \eta-premises by \Pi-Wf):

Case N-\beta-ze, N-\beta-su: analogous to \beta above. Apply ? statement (2) to the original reduction rule at \sigma to get equality at the contractum-substituted-by-\sigma. Then apply IH (statement (1)) to the typing of the contractum (derivable from the reduction rule and ?) to bridge the contractum from \sigma to \sigma'.

Case

By IH on the premise (with the roles of \sigma, \sigma' swapped): \tyequiv[\Gamma]{t[\sigma']}{t'[\sigma]}{T[\sigma']}. By ? statement (2), \tyequiv[\Gamma]{T[\sigma]} {T[\sigma']}{\ensuremath{\texttt{Ty}_{i}}} (from the reflexive closure on the type-formation of T via presupposition). By Tm-Subsump with Sub-Eq, transport to the goal type T[\sigma]: \tyequiv[\Gamma]{t'[\sigma]}{t[\sigma']}{T[\sigma]}, then apply Tm-Sym.

Case

By IH on the first premise: \tyequiv[\Gamma]{t[\sigma]}{t'[\sigma]}{T[\sigma]} (instantiated at \sigma \approx \sigma, reflexive). By IH on the second premise: \tyequiv[\Gamma]{t'[\sigma]}{t''[\sigma']}{T[\sigma]}. By Tm-Trans: \tyequiv[\Gamma]{t[\sigma]}{t''[\sigma']}{T[\sigma]}.

Case

Statement (3): subtyping preservation. By induction on the subtyping derivation.

Case Sub-Univ: \ensuremath{\texttt{Ty}_{i}}[\sigma] = \ensuremath{\texttt{Ty}_{i}}, \ensuremath{\texttt{Ty}_{j}}[\sigma'] = \ensuremath{\texttt{Ty}_{j}}, and the conclusion follows from Sub-Univ at i \le j (the same hypothesis), with \vdash \Gamma from \judge[\Gamma]{\sigma : \Delta}.

Case

Case Sub-Trans: by IH on both premises and Sub-Trans, using a shared middle subtype evaluated at \sigma on both sides.

Case Sub-Eq: by IH on the premise via statement (2) and Sub-Eq.

By ?, \typing[\Gamma]{s}{S[\sigma]} and \typing[\Gamma]{s'}{S[\sigma]} from \tyequiv[\Gamma]{s}{s'}{S[\sigma]}. Build the substitution equivalence \judge[\Gamma]{(\sigma, s/x) \approx (\sigma, s'/x) : (\Delta, x:S)}: at every y \in \Delta both sides yield \sigma(y), and at x the heads s, s' are equated at S[\sigma] by hypothesis. Apply ? statement (1) to \typing[\Delta, x:S]{T}{\ensuremath{\texttt{Ty}_{i}}}.

By mutual induction on the derivations. In each case, the conclusion follows because the rules are syntax-directed: no two rules apply to the same configuration.

Symmetry is immediate (swap the two conjuncts). Transitivity follows from determinism of readback (?).

Case \textsf{Ne}. Suppose e \approx e' \in \textsf{Ne} and e' \approx e'' \in \textsf{Ne}.

The cases for \textsf{Nf} and \textsf{Ty} are analogous, using determinism of \textsf{R}^{\textsf{Nf}} and \textsf{R}^{\textsf{Ty}} respectively.

By induction on the derivation.

Case

Symmetry and transitivity are immediate.

Case

Transitivity: given additionally \texttt{su}(a') \approx \texttt{su}(a'') \in \textsf{Nat} (hence a' \approx a'' \in \textsf{Nat}), by the IH a \approx a'' \in \textsf{Nat}, so \texttt{su}(a) \approx \texttt{su}(a'') \in \textsf{Nat}.

Case

Transitivity follows analogously from transitivity of \textsf{Ne}.

By induction on the derivation of a \approx a' \in \textsf{Nat}.

Case

Both sides read back to \textsf{zero} at every level n, so {\downarrow}^N(\texttt{ze}) \approx {\downarrow}^N(\texttt{ze}) \in \textsf{Nf}.

Case

Case

By induction on the derivation of A \approx A' \in \mathcal{U}_i \searrow R.

Case

The same derivation works at level j (neutrals are level-independent): {\uparrow}^A(b) \approx {\uparrow}^{A'}(b') \in \mathcal{U}_j \searrow R by U-Ne.

Case

Case

Level-independent: N \approx N \in \mathcal{U}_j \searrow R by U-Nat.

Case

By induction on the two derivations simultaneously. The cases are forced: N can only match \textsc{U-Nat}, a neutral can only match \textsc{U-Ne}, etc.

Case \textsc{U-Ne}.

Both derivations force R \Leftrightarrow \textsf{Neu} and R' \Leftrightarrow \textsf{Neu}, so R \Leftrightarrow R'.

Case \textsc{U-Nat}. Both derivations force R \Leftrightarrow \textsf{Nat} and R' \Leftrightarrow \textsf{Nat}, so R \Leftrightarrow R'.

Case \textsc{U-Univ}. Both derivations force R \Leftrightarrow \mathcal{U}_j and R' \Leftrightarrow \mathcal{U}_j, so R \Leftrightarrow R'.

Case \textsc{U-Pi}.

From the second derivation we get R_I' with A \approx A' \in \mathcal{U}_i \searrow R_I'.

By induction on the derivation. We prove both statements simultaneously.

Case

For (1):

For (2): Suppose a \approx a' \in R, i.e. a \approx a' \in \textsf{Neu} (since R \Leftrightarrow \textsf{Neu}). Then a = {\uparrow}^B(e) and a' = {\uparrow}^{B'}(e') with e \approx e' \in \textsf{Ne}. By symmetry of \textsf{Ne}, e' \approx e \in \textsf{Ne}, so a' \approx a \in \textsf{Neu}, i.e. a' \approx a \in R.

Case

For (1): Immediate (U_j \approx U_j is symmetric).

For (2): Suppose a \approx a' \in R, i.e. a \approx a' \in \mathcal{U}_j \searrow R_0 for some R_0. By the IH at level j (which is structurally smaller), a' \approx a \in \mathcal{U}_j \searrow R_0, so a' \approx a \in R.

Case

For (1): Immediate.

For (2): Suppose a \approx a' \in R, i.e. a \approx a' \in \textsf{Nat}. By symmetry of \textsf{Nat} (?), a' \approx a \in \textsf{Nat}, so a' \approx a \in R.

Case

For (1): We construct a U-Pi derivation of \Pi(A', T', \rho') \approx \Pi(A, T, \rho) \in \mathcal{U}_i \searrow R. We verify the four premises.

Premise 1 (domain):

Premise 2: R_I is a PER (by hypothesis).

Premise 3 (codomain): Let \ensuremath{\mathcal{D}}' :: a' \approx a \in R_I.

Define R_O'(\ensuremath{\mathcal{D}}') := R_O(\ensuremath{\mathrm{D}}_0).

Premise 4 (biconditional): We must show

Since R_I is a PER, the set of pairs \{(a, a') \mid a \approx a' \in R_I\} is closed under swapping: (a, a') \in R_I iff (a', a) \in R_I. By right irrelevance (?), R_O(\ensuremath{\mathcal{D}}) depends only on the pair (a, a'), not the specific evidence \ensuremath{\mathcal{D}}. Hence the right-hand side “\forall\, \ensuremath{\mathcal{D}}' :: a' \approx a \in R_I.\; f \cdot a' \approx f' \cdot a \in R_O'(\ensuremath{\mathcal{D}}')” is, after renaming bound variables (a' \mapsto b, a \mapsto b'), equivalent to “\forall\, \ensuremath{\mathcal{D}}'':: b \approx b' \in R_I.\; f \cdot b \approx f' \cdot b' \in R_O(\ensuremath{\mathcal{D}}'')” which is exactly the original right-hand side. Therefore the same R satisfies both biconditionals.

For (2): Suppose f \approx f' \in R. We must show f' \approx f \in R, i.e. for all \ensuremath{\mathcal{D}} :: a \approx a' \in R_I, f' \cdot a \approx f \cdot a' \in R_O(\ensuremath{\mathcal{D}}).

By induction on the two derivations. We must case-split on both; by the structure of the definition, matching cases are forced (e.g., N can only relate to N).

Case \textsc{U-Ne}.

and

Case \textsc{U-Nat} and \textsc{U-Univ}: immediate.

Case \textsc{U-Pi}. The first derivation is:

The second derivation is:

For (1): We construct a U-Pi derivation of \Pi(A_1, T_1, \rho_1) \approx \Pi(A_3, T_3, \rho_3) \in \mathcal{U}_i \searrow R.

Premise 1 (domain):

Premise 2: R_I is a PER (by hypothesis).

Premise 3 (codomain): Let \ensuremath{\mathcal{D}} :: a \approx a' \in R_I. We must show \ensuremath{\llbracket T_1 \rrbracket(\rho_1, a/x)} \approx \ensuremath{\llbracket T_3 \rrbracket(\rho_3, a'/x)} \in \mathcal{U}_i \searrow R_O''(\ensuremath{\mathcal{D}}) for some R_O''.

Set R_O''(\ensuremath{\mathcal{D}}) := R_O(\ensuremath{\mathrm{D}}_1).

Premise 4 (biconditional): We must show f \approx f' \in R \;\leftrightarrow\; (\forall\, \ensuremath{\mathcal{D}} :: a \approx a' \in R_I.\; f \cdot a \approx f' \cdot a' \in R_O''(\ensuremath{\mathcal{D}})). Since R_O''(\ensuremath{\mathcal{D}}) = R_O(\ensuremath{\mathrm{D}}_1) and by right irrelevance R_O(\ensuremath{\mathrm{D}}_1) \Leftrightarrow R_O(\ensuremath{\mathcal{D}}) (both have the same left type \ensuremath{\llbracket T_1 \rrbracket(\rho_1, a/x)}), the right-hand side is equivalent to the original biconditional for R. Hence the same R works.

For (2): Suppose f_1 \approx f_2 \in R and f_2 \approx f_3 \in R. We must show f_1 \approx f_3 \in R, i.e. for all \ensuremath{\mathcal{D}} :: a \approx a' \in R_I, f_1 \cdot a \approx f_3 \cdot a' \in R_O(\ensuremath{\mathcal{D}}).

By induction on the derivation of A \mathrel{<:_i} A'.

Case

Case

Case

Both sides are in \mathcal{U}_i (via U-Nat) returning \textsf{Nat}, and \textsf{Nat} \subseteq \textsf{Nat}.

Case

The domain PERs coincide by hypothesis. For the function PERs:

By induction on the derivation of A \mathrel{<:_i} B, with case analysis on the constructor of B \mathrel{<:_i} C that must agree on the shape of B.

Case

Here B = {\uparrow}^{B_0}(b'), so B \mathrel{<:_i} C must also be by <:-Ne, with C = {\uparrow}^{C_0}(b'') and b' \approx b'' \in \textsf{Ne}. By transitivity of the neutral PER (?), b \approx b'' \in \textsf{Ne}. By <:-Ne, {\uparrow}^{A_0}(b) \mathrel{<:_i} {\uparrow}^{C_0}(b'').

Case

Here B = U_k, so B \mathrel{<:_i} C must be by <:-Univ, with C = U_{k'}, k \le k', and k' < i. By transitivity of \le on \mathbb{N}, j \le k', and k' < i by hypothesis. By <:-Univ, U_j \mathrel{<:_i} U_{k'}.

Case

Here B = N, so B \mathrel{<:_i} C must be by <:-Nat with C = N. By <:-Nat, N \mathrel{<:_i} N.

Case

Here B = \Pi(B_I, T_B, \rho_B), so B \mathrel{<:_i} C must be by <:-Pi, with C = \Pi(C_I, T_C, \rho_C) and:

Domain. By ? applied to A_I \approx B_I \in \mathcal{U}_i \searrow R_I and B_I \approx C_I \in \mathcal{U}_i \searrow R_I': A_I \approx C_I \in \mathcal{U}_i, with output PER (call it R_I^*) determined up to logical equivalence by ?; in particular, R_I^* \Leftrightarrow R_I \Leftrightarrow R_I'.

Codomain. Let \ensuremath{\mathcal{D}}^* :: a \approx a' \in R_I^* be given. By the equivalence R_I^* \Leftrightarrow R_I, \ensuremath{\mathcal{D}}^* also witnesses a \approx a' \in R_I, and by R_I^* \Leftrightarrow R_I' it also witnesses some \ensuremath{\mathcal{D}}' :: a \approx a' \in R_I'. Apply the codomain hypothesis of the first derivation at this \ensuremath{\mathcal{D}}^* (used as \ensuremath{\mathcal{D}} in R_I):

Apply the codomain hypothesis of the second derivation at \ensuremath{\mathcal{D}}':

Since \ensuremath{\mathcal{D}}^* witnesses both pairs we have a' = a'' at this instantiation; the inductive hypothesis composes the two:

Self-relatedness. Already given: \Pi(A_I, T_A, \rho_A) \approx \Pi(A_I, T_A, \rho_A) \in \mathcal{U}_i from the first derivation and \Pi(C_I, T_C, \rho_C) \approx \Pi(C_I, T_C, \rho_C) \in \mathcal{U}_i from the second.

Conclusion. By <:-Pi with the four ingredients (domain in \mathcal{U}_i \searrow R_I^*, codomain pointwise subtyping at every \ensuremath{\mathcal{D}}^*, and the two self-relatedness facts):

By induction on A \approx A' \in \mathcal{U}_i.

U-Ne: A = {\uparrow}^{A_0}(b), A' = {\uparrow}^{A_0'}(b'), b \approx b' \in \textsf{Ne}. By <:-Ne. U-Univ: A = A' = U_j with j < i. By <:-Univ with j \le j. U-Nat: A = A' = N. By <:-Nat. U-Pi: A = \Pi(A_I, T, \rho), A' = \Pi(A_I', T', \rho'), domain A_I \approx A_I' \in \mathcal{U}_i \searrow R_I, codomain pointwise \ensuremath{\llbracket T \rrbracket(\rho, a/x)} \approx \ensuremath{\llbracket T' \rrbracket(\rho', a'/x)} \in \mathcal{U}_i, and self-relatedness of both Pi-types. By inner IH on the codomain \mathcal{U}_i-equality: \ensuremath{\llbracket T \rrbracket(\rho, a/x)} \mathrel{<:_i} \ensuremath{\llbracket T' \rrbracket(\rho', a'/x)}. By <:-Pi.

By simultaneous induction on the derivation of A \approx A' \in \mathcal{U}_i \searrow R. We also need an auxiliary lemma that a \approx a' \in \textsf{Nat} implies {\downarrow}^N(a) \approx {\downarrow}^N(a') \in \textsf{Nf}, which is ?.

Case

For (1): Since R \Leftrightarrow \textsf{Neu}, we have a = {\uparrow}^B(e) and a' = {\uparrow}^{B'}(e') with e \approx e' \in \textsf{Ne}. Reading back {\downarrow}^{{\uparrow}^A(b)}({\uparrow}^B(e)) at a neutral type reads e as a neutral (by Rf-ne), and both sides produce the same neutral normal form since e \approx e' \in \textsf{Ne}.

For (2): We need {\uparrow}^{{\uparrow}^A(b)}(e) \approx {\uparrow}^{{\uparrow}^{A'}(b')}(e') \in R. Since R \Leftrightarrow \textsf{Neu}, this reduces to e \approx e' \in \textsf{Ne}, which holds by hypothesis.

For (3): We must show {\uparrow}^A(b) \approx {\uparrow}^{A'}(b') \in \textsf{Ty}, i.e. reading back both sides as types produces the same result. Since b \approx b' \in \textsf{Ne}, reading both as neutrals produces the same neutral normal form.

Case

For (1): We have a \approx a' \in R, i.e. a \approx a' \in \mathcal{U}_j \searrow R_0 for some R_0. By IH (3) on the \mathcal{U}_j derivation (structurally smaller since j < i), a \approx a' \in \textsf{Ty}_j. Reading back {\downarrow}^{U_j}(a) as a normal form reads a as a type, hence {\downarrow}^{U_j}(a) \approx {\downarrow}^{U_j}(a') \in \textsf{Nf}.

For (2): We need {\uparrow}^{U_j}(e) \approx {\uparrow}^{U_j}(e') \in R, i.e. {\uparrow}^{U_j}(e) \approx {\uparrow}^{U_j}(e') \in \mathcal{U}_j \searrow R_0 for some R_0.

For (3): A = A' = U_j. Both sides read back to \ensuremath{\texttt{Ty}_{j}}.

Case

For (1): Since R \Leftrightarrow \textsf{Nat}, we have a \approx a' \in \textsf{Nat}. By ?, {\downarrow}^N(a) \approx {\downarrow}^N(a') \in \textsf{Nf}.

For (2): We need {\uparrow}^N(e) \approx {\uparrow}^N(e') \in \textsf{Nat}.

For (3): A = A' = N. Both sides read back to \ensuremath{\texttt{Nat}}.

Case

For (1): We have f \approx f' \in R, i.e. for all \ensuremath{\mathcal{D}} :: a \approx a' \in R_I, f \cdot a \approx f' \cdot a' \in R_O(\ensuremath{\mathcal{D}}). Reading back {\downarrow}^{\Pi(A_0,T,\rho)}(f) at level n:

The readback rule for \Pi-types assembles these into \textsf{R}^{\textsf{Nf}}_n({\downarrow}^{\Pi(A_0,T,\rho)}(f)) \searrow \lambda x.\, w and \textsf{R}^{\textsf{Nf}}_n({\downarrow}^{\Pi(A_0',T',\rho')}(f')) \searrow \lambda x.\, w with the same body w.

For (2): By the biconditional, we must show that for all \ensuremath{\mathcal{D}} :: a \approx a' \in R_I, ({\uparrow}^{\Pi(A_0,T,\rho)}(e)) \cdot a \approx ({\uparrow}^{\Pi(A_0',T',\rho')}(e')) \cdot a' \in R_O(\ensuremath{\mathcal{D}}).

For (3): Reading back \Pi(A_0, T, \rho) as a type at level n:

The type readback rule for \Pi-types reads back the domain and codomain separately; both agree by the above.

By induction on the first derivation.

Case

The second derivation also concludes \cdot \approx \cdot \searrow \top, so R = R' = \top and \top \Leftrightarrow \top.

Case The first derivation is:

The second derivation is:

We show R \Leftrightarrow R', i.e. \rho \approx \rho' \in R iff \rho \approx \rho' \in R'.

(\Rightarrow): Suppose \rho \approx \rho' \in R. By the first biconditional, we obtain \ensuremath{\mathcal{D}} :: \rho[\Uparrow] \approx \rho'[\Uparrow] \in R_T with \rho(0) \approx \rho'(0) \in R_H(\ensuremath{\mathcal{D}}).

(\Leftarrow): Symmetric, swapping the roles of the two derivations.

By induction on the derivation.

Case

Both statements are immediate (\top is symmetric).

Case

For (1): We construct a Ctx-Ext derivation of \Gamma', x : S' \approx \Gamma, x : S \searrow R. We verify each of the four premises.

Premise 1 (tail):

Premise 2: R_T is a PER (by hypothesis).

Premise 3 (head): Given \ensuremath{\mathcal{D}}' :: \rho' \approx \rho \in R_T, we must show \ensuremath{\llbracket S' \rrbracket(\rho')} \approx \ensuremath{\llbracket S \rrbracket(\rho)} \in \mathcal{U}_i \searrow R_H'(\ensuremath{\mathcal{D}}') for some R_H'.

Set R_H'(\ensuremath{\mathcal{D}}') := R_H(\ensuremath{\mathrm{D}}_0).

Premise 4 (biconditional): We must verify

The original biconditional states:

\ensuremath{\mathcal{D}} and \ensuremath{\mathcal{D}}' already discharge. Moreover R_H'(\ensuremath{\mathcal{D}}') = R_H(\ensuremath{\mathrm{D}}_0) \Leftrightarrow R_H(\ensuremath{\mathcal{D}}) by right irrelevance. Hence both biconditionals characterize the same R.

For (2): Suppose \rho \approx \rho' \in R. By the biconditional, there exists \ensuremath{\mathcal{D}} :: \rho[\Uparrow] \approx \rho'[\Uparrow] \in R_T with \rho(0) \approx \rho'(0) \in R_H(\ensuremath{\mathcal{D}}). We must show \rho' \approx \rho \in R, i.e. exhibit evidence for \rho'[\Uparrow] \approx \rho[\Uparrow] \in R_T together with the heads being related.

The tail evidence \ensuremath{\mathcal{D}}' and the head relatedness \rho'(0) \approx \rho(0) \in R_H(\ensuremath{\mathcal{D}}') together witness \rho' \approx \rho \in R by the biconditional.

By induction on the first derivation.

Case

Both statements are immediate (\top is transitive).

Case The first derivation is:

The second derivation is:

For (1): We construct a Ctx-Ext derivation of \Gamma_1, x : S_1 \approx \Gamma_3, x : S_3 \searrow R.

Premise 1 (tail):

Premise 2: R_T is a PER (by hypothesis).

Premise 3 (head): Given \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R_T, we must show \ensuremath{\llbracket S_1 \rrbracket(\rho)} \approx \ensuremath{\llbracket S_3 \rrbracket(\rho')} \in \mathcal{U}_i \searrow R_H''(\ensuremath{\mathcal{D}}).

Set R_H''(\ensuremath{\mathcal{D}}) := R_H(\ensuremath{\mathrm{D}}_1).

Premise 4 (biconditional): The biconditional characterizes the same R. Since R_T is a PER, the quantification ranges over the same set of pairs. By ?, R_H''(\ensuremath{\mathcal{D}}) \Leftrightarrow R_H(\ensuremath{\mathcal{D}}) (both have the same left type \ensuremath{\llbracket S_1 \rrbracket(\rho[\Uparrow])}), so the biconditional is equivalent to the original.

For (2): Suppose \rho_1 \approx \rho_2 \in R and \rho_2 \approx \rho_3 \in R. We must show \rho_1 \approx \rho_3 \in R, i.e. exhibit \ensuremath{\mathcal{D}} :: \rho_1[\Uparrow] \approx \rho_3[\Uparrow] \in R_T with \rho_1(0) \approx \rho_3(0) \in R_H(\ensuremath{\mathcal{D}}).

By the biconditional, from \rho_1 \approx \rho_2 \in R we get \ensuremath{\mathrm{D}}_1 :: \rho_1[\Uparrow] \approx \rho_2[\Uparrow] \in R_T with \rho_1(0) \approx \rho_2(0) \in R_H(\ensuremath{\mathrm{D}}_1). From \rho_2 \approx \rho_3 \in R we get \ensuremath{\mathrm{D}}_2 :: \rho_2[\Uparrow] \approx \rho_3[\Uparrow] \in R_T with \rho_2(0) \approx \rho_3(0) \in R_H(\ensuremath{\mathrm{D}}_2).

Hence \rho_1 \approx \rho_3 \in R by the biconditional (with witness \ensuremath{\mathcal{D}}).

By induction on the context subtyping derivation.

Case

Both R and R' are \top, so the inclusion is trivial.

Case

Suppose \rho \approx \rho' \in R. By ?, R \Leftrightarrow R_1 (both derive from \Gamma, x : S \approx \Gamma, x : S), so \rho \approx \rho' \in R_1. We must show \rho \approx \rho' \in R'. By ?, R' \Leftrightarrow R_2, so it suffices to show \rho \approx \rho' \in R_2.

By the biconditional of R_1: from \rho \approx \rho' \in R_1 we obtain \ensuremath{\mathcal{D}} :: \rho[\Uparrow] \approx \rho'[\Uparrow] \in R_T with \rho(0) \approx \rho'(0) \in R_H(\ensuremath{\mathcal{D}}), where \ensuremath{\llbracket S \rrbracket(\rho[\Uparrow])} \approx \ensuremath{\llbracket S \rrbracket(\rho'[\Uparrow])} \in \mathcal{U}_i \searrow R_H(\ensuremath{\mathcal{D}}).

By the IH on the tail: from \rho[\Uparrow] \approx \rho'[\Uparrow] \in R_T we get \rho[\Uparrow] \approx \rho'[\Uparrow] \in R_T' (where R_T' is the tail PER of R_2; call this evidence \ensuremath{\mathcal{D}}').

By the subtyping premise: \ensuremath{\llbracket S \rrbracket(\rho[\Uparrow])} \mathrel{<:_i} \ensuremath{\llbracket S' \rrbracket(\rho'[\Uparrow])}. By the head premise of R_2 at \ensuremath{\mathcal{D}}': \ensuremath{\llbracket S' \rrbracket(\rho[\Uparrow])} \approx \ensuremath{\llbracket S' \rrbracket(\rho'[\Uparrow])} \in \mathcal{U}_i \searrow R_H'(\ensuremath{\mathcal{D}}').

Hence \rho \approx \rho' \in R_2 by the biconditional of R_2 (with witness \ensuremath{\mathcal{D}}' and head \rho(0) \approx \rho'(0) \in R_H'(\ensuremath{\mathcal{D}}')), and thus \rho \approx \rho' \in R'.

By induction on the derivation of \Gamma \approx \Gamma \searrow R.

Case Ctx-Emp: R = \top, so any two environments are related.

Case Ctx-Ext: By the biconditional, we must exhibit \ensuremath{\mathcal{D}} :: {\uparrow}^\Gamma[\Uparrow] \approx {\uparrow}^\Gamma[\Uparrow] \in R_T with ({\uparrow}^\Gamma)(0) \approx ({\uparrow}^\Gamma)(0) \in R_H(\ensuremath{\mathcal{D}}).

Immediate because \ensuremath{\llbracket \ensuremath{\textsf{id}} \rrbracket(\rho)} = \rho for weakening.

Immediate by analyzing \Gamma, x : T \approx \Gamma, x : T \searrow R.

Immediate by the definition of composition.

By induction on \ensuremath{\vDash \Gamma}. The empty case follows from Ctx-Emp, giving \cdot \approx \cdot \searrow \top. The extension case directly returns the packaged (\Gamma, x : S) \approx (\Gamma, x : S) \searrow R.

We must show: for all \Gamma' \approx \Gamma' \searrow R', all \semweak[\Gamma']{\phi}{\Delta}, and all \rho \approx \rho' \in R',

Recall from ? that the evaluation of a weakening \psi in an environment \rho is defined by \ensuremath{\llbracket \psi \rrbracket(\rho)}(n) = \rho(\psi(n)), i.e., it reindexes the environment according to \psi. We compute each of the four values:

Hence \ensuremath{\llbracket \psi[\phi] \rrbracket(\rho)} = \ensuremath{\llbracket \psi \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})} — the commutation is definitional for weakenings. Similarly \ensuremath{\llbracket \psi[\phi] \rrbracket(\rho')} = \ensuremath{\llbracket \psi \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho')})}. So all four values collapse to two:

From \semweak[\Gamma']{\phi}{\Delta} and \rho \approx \rho' \in R', we have \ensuremath{\llbracket \phi \rrbracket(\rho)} \approx \ensuremath{\llbracket \phi \rrbracket(\rho')} \in R_\Delta. From \semweak[\Delta]{\psi}{\Gamma} and \ensuremath{\llbracket \phi \rrbracket(\rho)} \approx \ensuremath{\llbracket \phi \rrbracket(\rho')} \in R_\Delta, we have

Since all four values equal \ensuremath{\llbracket \psi \circ \phi \rrbracket(\rho)} or \ensuremath{\llbracket \psi \circ \phi \rrbracket(\rho')} (which equal the inner two by the above computation), the four-way relatedness follows by symmetry (?) and transitivity (?) of R_\Gamma.

By ? applied to \semweak[\Gamma]{\ensuremath{\textsf{id}}}{\Gamma} (which holds by ?).

By ? applied to \semweak[\Gamma, x:S]{\Uparrow}{\Gamma} (which holds by ?).

Instantiate \semtyeq[\Gamma]{t}{t'}{T} at \Gamma (with R_\Gamma), the identity semantic substitution \semtyeq[\Gamma]{\ensuremath{\textsf{id}}}{\ensuremath{\textsf{id}}}{\Gamma} (?), and \rho \approx \rho' \in R_\Gamma. Since T[\ensuremath{\textsf{id}}] = T, t[\ensuremath{\textsf{id}}] = t, t'[\ensuremath{\textsf{id}}] = t', and \ensuremath{\llbracket \ensuremath{\textsf{id}} \rrbracket(\rho)} = \rho, the four-value patterns for the type and term collapse to \ensuremath{\llbracket T \rrbracket(\rho)} \approx \ensuremath{\llbracket T \rrbracket(\rho')} \in \mathcal{U}_i \searrow R and \ensuremath{\llbracket t \rrbracket(\rho)} \approx \ensuremath{\llbracket t' \rrbracket(\rho')} \in R, respectively.

Let \Gamma' \approx \Gamma' \searrow R' be given, with \semweak[\Gamma']{\phi}{\Gamma} and \rho \approx \rho' \in R'. We must show:

We make two instantiations of the hypothesis \semtyeq[\Delta]{\sigma}{\sigma'}{\Delta'}.

First instantiation: at \Gamma', the composed semantic weakening \semweak[\Gamma']{\psi \circ \phi}{\Delta} (by ? from \semweak[\Gamma']{\phi}{\Gamma} and \semweak[\Gamma]{\psi}{\Delta}), and \rho \approx \rho' \in R':

Since (\sigma[\psi])[\phi] = \sigma[\psi \circ \phi] (by ?), the outer values are \ensuremath{\llbracket (\sigma[\psi])[\phi] \rrbracket(\rho)} and \ensuremath{\llbracket (\sigma'[\psi])[\phi] \rrbracket(\rho')}.

Second instantiation: at \Gamma with R_\Gamma, the semantic weakening \semweak[\Gamma]{\psi}{\Delta} (given), and \ensuremath{\llbracket \phi \rrbracket(\rho)} \approx \ensuremath{\llbracket \phi \rrbracket(\rho')} \in R_\Gamma (from \semweak[\Gamma']{\phi}{\Gamma} applied to \rho \approx \rho' \in R'):

The outer values here are \ensuremath{\llbracket \sigma[\psi] \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})} and \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho')})} — exactly the inner values of our goal.

Now observe: since \ensuremath{\llbracket \psi \circ \phi \rrbracket(\rho)} = \ensuremath{\llbracket \psi \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})} (weakenings commute with evaluation definitionally), the inner values of both instantiations coincide: \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \circ \phi \rrbracket(\rho)})} = \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})})}.

From the first instantiation: \ensuremath{\llbracket (\sigma[\psi])[\phi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})})} \in R_{\Delta'}. From the second instantiation: \ensuremath{\llbracket \sigma[\psi] \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})} \approx \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})})} \in R_{\Delta'}. By symmetry and transitivity of R_{\Delta'}, all four goal values are related:

Hence \{\ensuremath{\llbracket (\sigma[\psi])[\phi] \rrbracket(\rho)},\; \ensuremath{\llbracket \sigma[\psi] \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho)})},\; \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\ensuremath{\llbracket \phi \rrbracket(\rho')})},\; \ensuremath{\llbracket (\sigma'[\psi])[\phi] \rrbracket(\rho')}\} \subseteq R_{\Delta'}.

Let \Gamma' \approx \Gamma' \searrow R', \semweak[\Gamma']{\phi}{\Gamma}, and \rho \approx \rho' \in R' be given. We must show

By ? (2) and associativity (?): (\Uparrow \circ \sigma)[\phi] = (\Uparrow \circ \sigma) \circ \phi = \Uparrow \circ (\sigma \circ \phi) = \Uparrow \circ \sigma[\phi]. For any substitution \tau and any environment \rho_0, the pointwise definitions give

Hence \ensuremath{\llbracket \Uparrow \circ \tau \rrbracket(\rho_0)} = (\ensuremath{\llbracket \tau \rrbracket(\rho_0)})[\Uparrow] definitionally. Specialising:

and analogously for the primed pair. So it suffices to show

Apply \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta, x:T} at \Gamma', \phi, and \rho \approx \rho' \in R': writing R_{\Delta,x:T} for the context PER of \Delta, x:T,

By the biconditional of R_{\Delta,x:T} (from Ctx-Ext), every pair \rho_0 \approx \rho_0' \in R_{\Delta,x:T} satisfies \rho_0[\Uparrow] \approx \rho_0'[\Uparrow] \in R_\Delta. Applying this pairwise to the four R_{\Delta,x:T}-related values above yields the desired R_\Delta-relatedness of the four shifted values.

Let \Gamma' \approx \Gamma' \searrow R', \semweak[\Gamma']{\psi}{\Gamma}, and \rho \approx \rho' \in R' be given. We must show:

From the hypothesis \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} applied at \Gamma', \psi, and \rho' \approx \rho \in R' (using symmetry of R', ?):

This gives us \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho')} \approx \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \in R_\Delta and \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \approx \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho)} \in R_\Delta.

By symmetry of R_\Delta (?), we can reverse pairs. The four values \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho)}, \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})}, \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})}, \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho')} are then pairwise related in R_\Delta (by symmetry and transitivity), yielding the desired four-way relatedness.

Let \Gamma' \approx \Gamma' \searrow R', \semweak[\Gamma']{\psi}{\Gamma}, and \rho \approx \rho' \in R' be given. From the first hypothesis:

In particular, \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \approx \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \in R_\Delta.

From the second hypothesis applied at the same \Gamma', \psi, and \rho \approx \rho':

In particular, \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \approx \ensuremath{\llbracket \sigma'' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \in R_\Delta.

By transitivity of R_\Delta (?), using \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \approx \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \in R_\Delta and (after mediating through symmetry) \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \approx \ensuremath{\llbracket \sigma'' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \in R_\Delta, we get \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \approx \ensuremath{\llbracket \sigma'' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \in R_\Delta.

For the outer pair: by similar reasoning on the weakened substitutions, \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \in R_\Delta (from the first hypothesis) and \ensuremath{\llbracket \sigma'' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} \approx \ensuremath{\llbracket \sigma''[\psi] \rrbracket(\rho')} \in R_\Delta (from the second hypothesis). By transitivity, all four values are related in R_\Delta:

From \semweak[\Gamma]{\psi}{\Delta} we have \Gamma \approx \Gamma \searrow R_\Gamma and \Delta \approx \Delta \searrow R_\Delta. By ? on \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}: for every \ensuremath{\mathcal{D}}_\Delta :: \rho_0 \approx \rho_0' \in R_\Delta, there is R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta) with \ensuremath{\llbracket S \rrbracket(\rho_0)} \approx \ensuremath{\llbracket S \rrbracket(\rho_0')} \in \mathcal{U}_i \searrow R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta). By Ctx-Ext, this gives (\Delta, x:S) \approx (\Delta, x:S) \searrow R_{\Delta,S}.

By ?, \psi gives \semtyeq[\Gamma]{\psi}{\psi}{\Delta}. Applying \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma with this semantic substitution and any \rho_0 \approx \rho_0' \in R_\Gamma, the type part gives in particular \ensuremath{\llbracket S[\psi] \rrbracket(\rho_0)} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho_0)})} \in \mathcal{U}_i \searrow R_H^\Gamma (commutation). By Ctx-Ext, this yields (\Gamma, x:S[\psi]) \approx (\Gamma, x:S[\psi]) \searrow R_{\Gamma,S[\psi]}.

We must show: for all \rho \approx \rho' \in R_{\Gamma, S[\psi]}, \ensuremath{\llbracket q(\psi) \rrbracket(\rho)} \approx \ensuremath{\llbracket q(\psi) \rrbracket(\rho')} \in R_{\Delta, S}. By the biconditional of R_{\Delta, S}, we must exhibit evidence \ensuremath{\mathcal{D}} :: (\ensuremath{\llbracket q(\psi) \rrbracket(\rho)})[\Uparrow] \approx (\ensuremath{\llbracket q(\psi) \rrbracket(\rho')})[\Uparrow] \in R_\Delta with (\ensuremath{\llbracket q(\psi) \rrbracket(\rho)})(0) \approx (\ensuremath{\llbracket q(\psi) \rrbracket(\rho')})(0) \in R_H^\Delta(\ensuremath{\mathcal{D}}).

Tail.

From \rho \approx \rho' \in R_{\Gamma, S[\psi]}, by the biconditional of R_{\Gamma, S[\psi]}: \rho[\Uparrow] \approx \rho'[\Uparrow] \in R_\Gamma. From \semweak[\Gamma]{\psi}{\Delta}: \ensuremath{\llbracket \psi \rrbracket(\rho[\Uparrow])} \approx \ensuremath{\llbracket \psi \rrbracket(\rho'[\Uparrow])} \in R_\Delta. This gives evidence \ensuremath{\mathcal{D}}.

Head.

From \rho \approx \rho' \in R_{\Gamma, S[\psi]}, by the biconditional of R_{\Gamma, S[\psi]}, there exists evidence \ensuremath{\mathcal{D}}' such that \rho(0) \approx \rho'(0) \in R_H^\Gamma(\ensuremath{\mathcal{D}}'), where R_H^\Gamma comes from \ensuremath{\llbracket S[\psi] \rrbracket(\rho[\Uparrow])} \approx \ensuremath{\llbracket S[\psi] \rrbracket(\rho'[\Uparrow])} \in \mathcal{U}_i \searrow R_H^\Gamma(\ensuremath{\mathcal{D}}').

By the head premise of R_{\Delta, S} at \ensuremath{\mathcal{D}} (using \ensuremath{\llbracket \psi \rrbracket(\rho[\Uparrow])} \approx \ensuremath{\llbracket \psi \rrbracket(\rho'[\Uparrow])} \in R_\Delta): \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho[\Uparrow])})} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho'[\Uparrow])})} \in \mathcal{U}_i \searrow R_H^\Delta(\ensuremath{\mathcal{D}}).

From the semantic well-formedness \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}, instantiated as above (at \Gamma, \semtyeq[\Gamma]{\psi}{\psi}{\Delta}, \rho[\Uparrow] \approx \rho'[\Uparrow]), the type part gives in particular the commutation \ensuremath{\llbracket S[\psi] \rrbracket(\rho[\Uparrow])} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho[\Uparrow])})} \in \mathcal{U}_i. By ?, R_H^\Gamma(\ensuremath{\mathcal{D}}') \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}) (both have the same left-hand domain type up to \Leftrightarrow). Hence \rho(0) \approx \rho'(0) \in R_H^\Delta(\ensuremath{\mathcal{D}}).

From \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} we have \Delta \approx \Delta \searrow R_\Delta. By ? on \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}: for every \ensuremath{\mathcal{D}}_\Delta :: \rho_0 \approx \rho_0' \in R_\Delta, there is R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta) with \ensuremath{\llbracket S \rrbracket(\rho_0)} \approx \ensuremath{\llbracket S \rrbracket(\rho_0')} \in \mathcal{U}_i \searrow R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta). By Ctx-Ext, this gives (\Delta, x:S) \approx (\Delta, x:S) \searrow R_{\Delta,x:S}.

Let \Gamma' \approx \Gamma' \searrow R', \semweak[\Gamma']{\psi}{\Gamma}, and \rho \approx \rho' \in R' be given. We must show:

Each of the four environments has the form (tail, head): the tail is the value of the underlying substitution on \Delta, and the head is the value at position x. By the biconditional of R_{\Delta, x:S}, it suffices to show the tails are pairwise related in R_\Delta (yielding evidence \ensuremath{\mathcal{D}}) and the heads are related in R_H^\Delta(\ensuremath{\mathcal{D}}).

Tails. Since (\sigma, t/x)[\psi] = (\sigma[\psi], t[\psi]/x) (by ?), the four tail environments are:

From \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} instantiated at \Gamma', \psi, and \rho \approx \rho' \in R':

In particular, the outer pair gives evidence \ensuremath{\mathcal{D}} :: \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho')} \in R_\Delta.

Heads. The four heads are:

We must show they are related in R_H^\Delta(\ensuremath{\mathcal{D}}), where R_H^\Delta(\ensuremath{\mathcal{D}}) comes from

From \semtyeq[\Gamma]{t}{t'}{S[\sigma]} at \Gamma', \psi, \rho \approx \rho' \in R', the type part gives some R_t with \ensuremath{\llbracket \rrbracket(\rho)} \approx \ensuremath{\llbracket S[\sigma] \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \in \mathcal{U}_i \searrow R_t (and analogous primed versions), and the term part gives

It remains to show R_t \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}). Note that \ensuremath{\llbracket \rrbracket(\rho)} = \ensuremath{\llbracket S[\sigma[\psi]] \rrbracket(\rho)} (by ?). By ?, we have \semtyeq[\Gamma']{\sigma[\psi]}{\sigma'[\psi]}{\Delta}. Instantiating \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', this semantic substitution, and \rho \approx \rho' \in R': the type part gives the commutation

Hence R_t (from \ensuremath{\llbracket S[\sigma[\psi]] \rrbracket(\rho)}) and R_H^\Delta(\ensuremath{\mathcal{D}}) (from \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)})}) have related left-hand types in \mathcal{U}_i; by ?, R_t \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}). Therefore the four heads are in R_H^\Delta(\ensuremath{\mathcal{D}}).

By ? on \semtyeq[\Delta]{t}{t'}{T}, for any \rho_0 \approx \rho_0' \in R_\Delta: \ensuremath{\llbracket T \rrbracket(\rho_0)} \approx \ensuremath{\llbracket T \rrbracket(\rho_0')} \in \mathcal{U}_i \searrow R_H^\Delta. By Ctx-Ext, this yields (\Delta, x:T) \approx (\Delta, x:T) \searrow R_{\Delta,x:T}.

Let \Gamma' \approx \Gamma' \searrow R', \semweak[\Gamma']{\psi}{\Gamma}, and \rho \approx \rho' \in R' be given. We must show:

By the biconditional of R_{\Delta, x:T} (with respect to the substitution extensions (\sigma, t[\sigma]/x), etc.), it suffices to exhibit evidence \ensuremath{\mathcal{D}} :: \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho')} \in R_\Delta — relating the tails of the outer pair of substitution evaluations — and to show that the four head values \ensuremath{\llbracket t[\sigma][\psi] \rrbracket(\rho)}, \ensuremath{\llbracket t[\sigma] \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})}, \ensuremath{\llbracket t'[\sigma'] \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})}, \ensuremath{\llbracket t'[\sigma'][\psi] \rrbracket(\rho')} are pairwise related in the head PER R_H^\Delta(\ensuremath{\mathcal{D}}), which is the PER returned by \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)})} \approx \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho')})} \in \mathcal{U}_i \searrow R_H^\Delta(\ensuremath{\mathcal{D}}).

Tails.

So the four tails are \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)}, \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})}, \ensuremath{\llbracket \sigma' \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})}, \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho')}. By \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} at \Gamma', \psi, \rho \approx \rho':

with witness \ensuremath{\mathcal{D}} :: \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho')} \in R_\Delta.

Heads. We instantiate \semtyeq[\Delta]{t}{t'}{T} in two ways and bridge the resulting four-value patterns through a shared inner value.

First instantiation of \semtyeq[\Delta]{t}{t'}{T}: at \Gamma', the semantic substitution \semtyeq[\Gamma']{\sigma[\psi]}{\sigma'[\psi]}{\Delta} (?), and \rho \approx \rho' \in R'. The type part gives some R_t with

and the term part gives

By ? (same left type \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)})}), R_t \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}). By ?, t[\sigma][\psi] = t[\sigma[\psi]], so the outer values match: \ensuremath{\llbracket t[\sigma][\psi] \rrbracket(\rho)} = \ensuremath{\llbracket t[\sigma[\psi]] \rrbracket(\rho)} (and similarly for the primed side). Hence the outer pair of goal heads and the inner pair \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)})}, \ensuremath{\llbracket t' \rrbracket(\ensuremath{\llbracket \sigma'[\psi] \rrbracket(\rho')})} are all in R_H^\Delta(\ensuremath{\mathcal{D}}).

Second instantiation of \semtyeq[\Delta]{t}{t'}{T}: at \Gamma (with R_\Gamma, from \semweak[\Gamma']{\psi}{\Gamma}), the semantic substitution \sigma \approx \sigma' : \Delta (the hypothesis), and \ensuremath{\llbracket \psi \rrbracket(\rho)} \approx \ensuremath{\llbracket \psi \rrbracket(\rho')} \in R_\Gamma. The type part gives some R_t' with

and the term part gives

Since \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)} and \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} are both in R_\Delta (related by the tails part), by ? applied to the two type evaluations (the head premise of R_{\Delta, x:T} at the appropriate evidence), R_t' \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}). This places the inner pair \ensuremath{\llbracket t[\sigma] \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})}, \ensuremath{\llbracket t'[\sigma'] \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho')})} of goal heads in R_H^\Delta(\ensuremath{\mathcal{D}}).

Bridging the two instantiations. The shared inner value \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})})} appears in both R_t (as the inner-left of the first instantiation, after using \ensuremath{\llbracket \sigma[\psi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})} \in R_\Delta and right irrelevance) and R_t' (as the inner-left of the second instantiation). Both R_t and R_t' are equivalent to R_H^\Delta(\ensuremath{\mathcal{D}}), so by transitivity of R_H^\Delta(\ensuremath{\mathcal{D}}) through this shared value, all four goal heads are related.

By ? on \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} and \semtyeq[\Delta]{t}{t'}{T}:

Apply ? again with this semantic substitution and \semtyeq[\Delta, x : T]{s}{s'}{S}:

We first establish the context PER for \Gamma, x:S[\sigma]. From \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} we have \Gamma \approx \Gamma \searrow R_\Gamma. Apply \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma (with R_\Gamma), the semantic substitution \semtyeq[\Gamma]{\sigma}{\sigma}{\Delta} (the reflexive instance, obtained from \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} via symmetry and transitivity, ?, ?), and any \ensuremath{\mathcal{D}}_\Gamma :: \rho_0 \approx \rho_0' \in R_\Gamma: the type part gives, in particular, \ensuremath{\llbracket S[\sigma] \rrbracket(\rho_0)} \approx \ensuremath{\llbracket S[\sigma] \rrbracket(\rho_0')} \in \mathcal{U}_i \searrow R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma) for some head family R_H^\Gamma. By Ctx-Ext, this yields (\Gamma, x:S[\sigma]) \approx (\Gamma, x:S[\sigma]) \searrow R_{\Gamma, x:S[\sigma]} with the biconditional

By an analogous construction (or directly by ? on \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} followed by Ctx-Ext), we also obtain (\Delta, x:S) \approx (\Delta, x:S) \searrow R_{\Delta, x:S} with head family R_H^\Delta, where for every \ensuremath{\mathcal{D}}_\Delta :: \rho_0 \approx \rho_0' \in R_\Delta, R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta) is determined by \ensuremath{\llbracket S \rrbracket(\rho_0)} \approx \ensuremath{\llbracket S \rrbracket(\rho_0')} \in \mathcal{U}_i \searrow R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta), with biconditional

Here R_\Delta comes from the premise \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta} (which carries \Delta \approx \Delta \searrow R_\Delta).

We now show \semtyeq[\Gamma, x:S[\sigma]]{q(\sigma)}{q(\sigma')}{\Delta, x:S} by unfolding the conclusion. Recall q(\sigma) = (\sigma[\Uparrow], x_0/x). By ? (2), (\sigma[\Uparrow], x_0/x)[\psi] = (\sigma[\Uparrow][\psi], x_0[\psi]/x) = (\sigma[\Uparrow \circ \psi], \psi(0)/x) for any weakening \psi (using \sigma[\Uparrow][\psi] = \sigma[\Uparrow \circ \psi] by associativity of post-composition with weakenings, and x_0[\psi] = \psi(0)).

We must show: for every context \Gamma' with \Gamma' \approx \Gamma' \searrow R', every \semweak[\Gamma']{\psi}{\Gamma, x:S[\sigma]}, and every \rho \approx \rho' \in R', the four values

lie in R_{\Delta, x:S}.

By definition of \semweak[\Gamma']{\psi}{\Gamma, x:S[\sigma]}, \ensuremath{\llbracket \psi \rrbracket(\rho)} \approx \ensuremath{\llbracket \psi \rrbracket(\rho')} \in R_{\Gamma, x:S[\sigma]}. By the biconditional of R_{\Gamma, x:S[\sigma]} established above, this gives

By ?, \semweak[\Gamma, x:S[\sigma]]{\Uparrow}{\Gamma}. By ?, \semweak[\Gamma']{\Uparrow \circ \psi}{\Gamma}, where \Uparrow \circ \psi is the composition of weakenings.

We must show the goal four values lie in R_{\Delta, x:S}. By the biconditional of R_{\Delta, x:S} recalled above, this requires evidence \ensuremath{\mathcal{D}}_\Delta relating the four tails in R_\Delta and the four heads in R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta).

Tails. We compute the four tails using the pointwise identities above. For an extended substitution (\tau, t/x), the evaluation \ensuremath{\llbracket (\tau, t/x) \rrbracket(\rho_0)} is the environment with head \ensuremath{\llbracket t \rrbracket(\rho_0)} at index 0 and tail \ensuremath{\llbracket \tau \rrbracket(\rho_0)} at indices 1, 2, \ldots; hence (\ensuremath{\llbracket (\tau, t/x) \rrbracket(\rho_0)})[\Uparrow] = \ensuremath{\llbracket \tau \rrbracket(\rho_0)}. Applied to the four goal values:

First instantiation of \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta}: at \Gamma', the semantic weakening \semweak[\Gamma']{\Uparrow \circ \psi}{\Gamma}, and \rho \approx \rho' \in R':

Since \Uparrow \circ \psi is a weakening, by the definition of weakening evaluation, \ensuremath{\llbracket \Uparrow \circ \psi \rrbracket(\rho_0)} = (\ensuremath{\llbracket \psi \rrbracket(\rho_0)})[\Uparrow] for any \rho_0 (verified pointwise: \ensuremath{\llbracket \Uparrow \circ \psi \rrbracket(\rho_0)}(n) = \rho_0((\Uparrow \circ \psi)(n)) = \rho_0(\psi(n+1)) = (\ensuremath{\llbracket \psi \rrbracket(\rho_0)})[\Uparrow](n)). So this first instantiation gives the outer two tails of the goal, plus intermediate values \ensuremath{\llbracket \sigma \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow])} and \ensuremath{\llbracket \sigma' \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho')})[\Uparrow])}.

Second instantiation of \semtyeq[\Gamma]{\sigma}{\sigma'}{\Delta}: at \Gamma, x:S[\sigma] (using R_{\Gamma, x:S[\sigma]}), the semantic weakening \semweak[\Gamma, x:S[\sigma]]{\Uparrow}{\Gamma}, and the related environments \ensuremath{\llbracket \psi \rrbracket(\rho)} \approx \ensuremath{\llbracket \psi \rrbracket(\rho')} \in R_{\Gamma, x:S[\sigma]}:

Since \Uparrow is a weakening, \ensuremath{\llbracket \Uparrow \rrbracket(\rho_0)} = \rho_0[\Uparrow] for any \rho_0. So this second instantiation gives the inner two tails of the goal, plus the intermediate values \ensuremath{\llbracket \sigma \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow])} and \ensuremath{\llbracket \sigma' \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho')})[\Uparrow])}.

The intermediate inner-left value \ensuremath{\llbracket \sigma \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow])} appears in both instantiations (since \ensuremath{\llbracket \Uparrow \circ \psi \rrbracket(\rho)} = (\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow] = \ensuremath{\llbracket \Uparrow \rrbracket(\ensuremath{\llbracket \psi \rrbracket(\rho)})}). By symmetry (?) and transitivity (?) of R_\Delta through this shared value, all four tails are pairwise related in R_\Delta. In particular, the outer pair gives evidence \ensuremath{\mathcal{D}}_\Delta :: \ensuremath{\llbracket \sigma[\Uparrow \circ \psi] \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma'[\Uparrow \circ \psi] \rrbracket(\rho')} \in R_\Delta.

Heads. The four heads of the goal four values are:

and analogously for the primed pair. All four heads collapse to (\ensuremath{\llbracket \psi \rrbracket(\rho)})(0) and (\ensuremath{\llbracket \psi \rrbracket(\rho')})(0). By the head clause of the biconditional of R_{\Gamma, x:S[\sigma]} recalled above, (\ensuremath{\llbracket \psi \rrbracket(\rho)})(0) \approx (\ensuremath{\llbracket \psi \rrbracket(\rho')})(0) \in R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma).

Bridging head PERs. It remains to show R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma) \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta), so that the four heads all lie in R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta). Apply \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma (using R_\Gamma, available from \semweak[\Gamma, x:S[\sigma]]{\Uparrow}{\Gamma}), the semantic substitution \semtyeq[\Gamma]{\sigma}{\sigma}{\Delta} (a special case of the hypothesis — formally, applying the hypothesis along with reflexivity by symmetry/transitivity to obtain the reflexive instance), and the related environments (\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow] \approx (\ensuremath{\llbracket \psi \rrbracket(\rho')})[\Uparrow] \in R_\Gamma (from \ensuremath{\mathcal{D}}_\Gamma): the type part gives the commutation

The right-hand side is \ensuremath{\llbracket S \rrbracket(\rho_0)} where \rho_0 = \ensuremath{\llbracket \sigma \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow])}, which is in R_\Delta via the second instantiation; by definition of R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta), this lands in \mathcal{U}_i \searrow R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta). The left-hand side \ensuremath{\llbracket S[\sigma] \rrbracket((\ensuremath{\llbracket \psi \rrbracket(\rho)})[\Uparrow])} lands in \mathcal{U}_i \searrow R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma) by definition of R_H^\Gamma. By ?, R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma) \Leftrightarrow R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta). Hence all four heads are in R_H^\Delta(\ensuremath{\mathcal{D}}_\Delta).

Combining tails and heads via the biconditional of R_{\Delta, x:S}, the four goal values are in R_{\Delta, x:S}.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R'. From the hypothesis:

We need:

Apply the hypothesis at \sigma' \approx \sigma (using ?) and \rho' \approx \rho (using symmetry of R'):

By symmetry of R_T (?), we can reverse the order:

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R'.

Apply the first hypothesis at \sigma \approx \sigma', \rho \approx \rho':

Apply the second hypothesis at \sigma' \approx \sigma' (reflexive, by ?, ?) and \rho' \approx \rho' (reflexive, by symmetry of R'):

By transitivity of R_T (?):

This is the outer-LHS vs outer-RHS of the goal’s four-value pattern. The other three pairs follow by combining the first hypothesis (giving \ensuremath{\llbracket t[\sigma] \rrbracket(\rho)}, \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})}, \ensuremath{\llbracket t' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})}, \ensuremath{\llbracket t'[\sigma'] \rrbracket(\rho')} pairwise in R_T) with the above transitivity step.

By Sem-Ctx-Emp of ?.

By ? on \ensuremath{\vDash \Gamma}, \Gamma \approx \Gamma \searrow R_T for some R_T. By ? on \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}, for any \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R_T, \ensuremath{\llbracket S \rrbracket(\rho)} \approx \ensuremath{\llbracket S \rrbracket(\rho')} \in \mathcal{U}_i \searrow R_H(\ensuremath{\mathcal{D}}). By Ctx-Ext of ?, this gives (\Gamma, x:S) \approx (\Gamma, x:S) \searrow R for some R. By Sem-Ctx-Ext of ?, applied to \ensuremath{\vDash \Gamma}, this context PER, and \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}, we conclude \ensuremath{\vDash \Gamma, x:S}.

By ?, \Gamma \approx \Gamma \searrow R for some R. Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. We must exhibit R_T such that

and

Type part. Since \ensuremath{\texttt{Ty}_{1+i}} is closed (it has no free variables), we compute:

Identical computations apply to the other two type values. Hence all four type values collapse to U_{1+i}, and we need U_{1+i} \approx U_{1+i} \in \mathcal{U}_{2+i} \searrow R_T for some R_T.

Term part. Since \ensuremath{\texttt{Ty}_{i}} is closed, the same computation gives

and similarly for the primed values, so all four term values collapse to U_i. Since R_T \Leftrightarrow \mathcal{U}_{1+i}, it suffices to show U_i \approx U_i \in \mathcal{U}_{1+i}, i.e. \exists R_0.\; U_i \approx U_i \in \mathcal{U}_{1+i} \searrow R_0.

Hence U_i \approx U_i \in R_T, and the four-value pattern follows.

By ?, \Gamma \approx \Gamma \searrow R for some R. Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. We must exhibit R_T such that

and

Type part. Since \ensuremath{\texttt{Ty}_{0}} is closed, we compute:

Identical computations give the same value for the other two type values. All four type values collapse to U_0, and we need U_0 \approx U_0 \in \mathcal{U}_1 \searrow R_T.

Term part. Since \ensuremath{\texttt{Nat}} is closed, all four term values collapse to N:

Since R_T \Leftrightarrow \mathcal{U}_0, it suffices to show N \approx N \in \mathcal{U}_0, i.e. \exists R_0.\; N \approx N \in \mathcal{U}_0 \searrow R_0.

Hence N \approx N \in R_T, and the four-value pattern follows.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. We must show that the four type values

for some R_T with R_T \Leftrightarrow \mathcal{U}_i (as in ?), and that the four term values

i.e. relate in \mathcal{U}_i \searrow R for some R.

Type part. As in ?, the four values of \ensuremath{\texttt{Ty}_{i}} collapse to U_i, and U_i \approx U_i \in \mathcal{U}_{1+i} \searrow R_T with R_T \Leftrightarrow \mathcal{U}_i by U-Univ.

Term part. We compute the four term values:

Analogous computations apply to the primed pair, yielding

We construct a U-Pi derivation relating the outermost two values; the inner two follow analogously.

Domain. Apply \semtyeq[\Gamma]{S}{S'}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', \sigma \approx \sigma' : \Gamma, and \rho \approx \rho' \in R':

Codomain via lifting. By ? on \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \semtyeq[\Gamma]{S}{S'}{\ensuremath{\texttt{Ty}_{i}}} (using its reflexive instance \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} via ?, ? for the well-formedness premise of ?):

By the first premise of the semantic substitution judgment, this carries (\Gamma', x:S[\sigma]) \approx (\Gamma', x:S[\sigma]) \searrow R_{\Gamma',x:S[\sigma]} and (\Gamma, x:S) \approx (\Gamma, x:S) \searrow R_{\Gamma,x:S}.

Let \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I be given. By the biconditional of R_{\Gamma',x:S[\sigma]} from Ctx-Ext, (\rho, a/x) \approx (\rho', a'/x) \in R_{\Gamma',x:S[\sigma]} requires \rho \approx \rho' \in R' (which we have) and a \approx a' \in R_H'(\ensuremath{\mathcal{D}}') where R_H' is the head family for R_{\Gamma',x:S[\sigma]}, governed by \ensuremath{\llbracket S[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket S[\sigma] \rrbracket(\rho')} \in \mathcal{U}_i \searrow R_H'(\ensuremath{\mathcal{D}}') (with \ensuremath{\mathcal{D}}' :: \rho \approx \rho' \in R'). By ? on the same left type \ensuremath{\llbracket S[\sigma] \rrbracket(\rho)} that governs both R_I (from the domain step) and R_H'(\ensuremath{\mathcal{D}}'), R_I \Leftrightarrow R_H'(\ensuremath{\mathcal{D}}'). Hence a \approx a' \in R_H'(\ensuremath{\mathcal{D}}'), and (\rho, a/x) \approx (\rho', a'/x) \in R_{\Gamma',x:S[\sigma]}.

Apply \semtyeq[\Gamma, x:S]{T}{T'}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', x:S[\sigma] (with R_{\Gamma',x:S[\sigma]}), the lifted substitution \semtyeq[\Gamma', x:S[\sigma]]{q(\sigma)}{q(\sigma')}{\Gamma, x:S}, and (\rho, a/x) \approx (\rho', a'/x) \in R_{\Gamma',x:S[\sigma]}:

The outer two values \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, a/x))} and \ensuremath{\llbracket T'[q(\sigma')] \rrbracket((\rho', a'/x))} are exactly the codomain expressions of the outer \Pi-values applied to a, a', satisfying the U-Pi codomain premise for the outer pair.

For the inner \Pi-values \Pi(\ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})}, T, \ensuremath{\llbracket \sigma \rrbracket(\rho)}) (left) and \Pi(\ensuremath{\llbracket S' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})}, T', \ensuremath{\llbracket \sigma' \rrbracket(\rho')}) (right), the codomain expressions applied to a, a' are \ensuremath{\llbracket T \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a/x))} and \ensuremath{\llbracket T' \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))}. Applying the lifted-substitution four-value pattern (instantiated at the identity weakening on \Gamma', x:S[\sigma] with (\rho, a/x) \approx (\rho', a'/x)), we obtain in particular

(the outer-versus-inner relatedness in that four-value pattern). By ? on \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} applied to this related pair:

Combined with the inner-pair relatedness from the codomain four-value pattern

and the analogous identity

on the primed side (by ? on the reflexive \semtyeq[\Gamma, x:S]{T'}{T'}{\ensuremath{\texttt{Ty}_{i}}} obtained from \semtyeq[\Gamma, x:S]{T}{T'}{\ensuremath{\texttt{Ty}_{i}}} by symmetry/transitivity), symmetry and transitivity of \mathcal{U}_i yield

This is the U-Pi codomain premise for the inner pair.

Function PER. Define R by the biconditional: f \approx f' \in R \;\leftrightarrow\; (\forall \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I.\; f \cdot a \approx f' \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I)).

Outer pair. By U-Pi applied with domain R_I (from Domain) and codomain R_O(\ensuremath{\mathcal{D}}_I) (from the outer pair of the codomain four-value pattern):

Inner pair. By U-Pi applied with domain R_I (the inner pair \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \approx \ensuremath{\llbracket S' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \in \mathcal{U}_i from Domain also lands in R_I by ?) and codomain R_O(\ensuremath{\mathcal{D}}_I) (just derived for the inner pair):

Cross-relations. We have established \Pi-relatedness for the outer pair and for the inner pair, both with element PER R. To get full four-way relatedness, we establish one cross-relation (outer-left versus inner-left) via a third U-Pi derivation; the remaining cross-relations follow by symmetry (?) and transitivity (?) of \mathcal{U}_i.

The third U-Pi derivation uses:

Domain. From the Domain four-value pattern (in \mathcal{U}_i \searrow R_I), the cross relation

\ensuremath{\llbracket S[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \in \mathcal{U}_i

holds, with element PER R_I by ?. Codomain. Let \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I. We must show

\ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, a/x))} \approx \ensuremath{\llbracket T \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a'/x))} \in \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I).

From the codomain four-value pattern, the cross relation

\ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, a/x))} \approx \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket q(\sigma') \rrbracket((\rho', a'/x))})} \in \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I)

holds (outer-left versus inner-right). By ? applied at the relatedness \ensuremath{\llbracket q(\sigma') \rrbracket((\rho', a'/x))} \approx (\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a'/x) \in R_{\Gamma, x:S} (which holds by symmetry and transitivity in R_{\Gamma, x:S}, bridging through the inner-pair relatedness of the lifted substitution four-value pattern):

\ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket q(\sigma') \rrbracket((\rho', a'/x))})} \approx \ensuremath{\llbracket T \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a'/x))} \in \mathcal{U}_i.

By transitivity of \mathcal{U}_i, \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, a/x))} \approx \ensuremath{\llbracket T \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a'/x))} \in \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I).

This is the outer-left \approx inner-left cross-relation. By symmetry and transitivity of \mathcal{U}_i combined with the outer-pair and inner-pair relations, all six pairs among the four \Pi-values are related in \mathcal{U}_i \searrow R.

Hence all four \Pi-values lie pairwise in \mathcal{U}_i \searrow R.

By induction on the lookup derivation x : T \in \Gamma, with \Gamma', R', \sigma, \sigma', \rho, \rho', and the witness \ensuremath{\mathcal{D}} fixed throughout.

Case

Here \Gamma = \Delta, x_0 : S, x = x_0, and T = S[\Uparrow]. Inverting \ensuremath{\vDash \Delta, x_0 : S} via Sem-Ctx-Ext gives \ensuremath{\vDash \Delta}, the packaged context PER (\Delta, x_0 : S) \approx (\Delta, x_0 : S) \searrow R_\Gamma, and \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} for some i. Inverting the context PER via Ctx-Ext gives \Delta \approx \Delta \searrow R_\Delta, a head family R_H with \ensuremath{\llbracket S \rrbracket(\rho_0)} \approx \ensuremath{\llbracket S \rrbracket(\rho_0')} \in \mathcal{U}_i \searrow R_H(\ensuremath{\mathcal{D}}_\Delta) for \ensuremath{\mathcal{D}}_\Delta :: \rho_0 \approx \rho_0' \in R_\Delta, and the biconditional

Instantiate \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} at \Gamma', \semweak[\Gamma']{\ensuremath{\textsf{id}}}{\Gamma'} (?), and \ensuremath{\mathcal{D}}: using \sigma[\ensuremath{\textsf{id}}] = \sigma and \ensuremath{\llbracket \ensuremath{\textsf{id}} \rrbracket(\rho)} = \rho we obtain \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma. By the biconditional of R_\Gamma, there exists \ensuremath{\mathcal{D}}_\Delta with

Set R_T := R_H(\ensuremath{\mathcal{D}}_\Delta).

Type part. We must show \{\ensuremath{\llbracket \rrbracket(\rho)},\; \ensuremath{\llbracket S[\Uparrow] \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})},\; \ensuremath{\llbracket S[\Uparrow] \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})},\; \ensuremath{\llbracket \rrbracket(\rho')}\} \subseteq \mathcal{U}_i \searrow R_T. We obtain this by two instantiations of \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}, bridged through a shared inner value.

By ?, \Gamma \approx \Gamma \searrow R_\Gamma. By ?, \semweak[\Gamma]{\Uparrow}{\Delta}. By ? on \semweak[\Gamma]{\Uparrow}{\Delta} and \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}: \semtyeq[\Gamma']{\Uparrow \circ \sigma}{\Uparrow \circ \sigma'}{\Delta}.

First instantiation. Apply \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', \semtyeq[\Gamma']{\Uparrow \circ \sigma}{\Uparrow \circ \sigma'}{\Delta}, and \ensuremath{\mathcal{D}}: for some R_1,

By ? (1), = S[\Uparrow \circ \sigma], so the outer values of the first instantiation match the goal’s outer values.

Second instantiation. By ? on \semweak[\Gamma]{\Uparrow}{\Delta}: \semtyeq[\Gamma]{\Uparrow}{\Uparrow}{\Delta}. From \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} at \Gamma', \ensuremath{\textsf{id}}, \ensuremath{\mathcal{D}}: \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma. Apply \semtyeq[\Delta]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma (using R_\Gamma), \semtyeq[\Gamma]{\Uparrow}{\Uparrow}{\Delta}, and \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma: for some R_2,

The outer values here are exactly the goal’s inner values.

Bridge. We have already established \ensuremath{\llbracket \Uparrow \circ \sigma \rrbracket(\rho_0)} = \ensuremath{\llbracket \Uparrow \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho_0)})} (from the proof of ?). Hence the inner-left values of both instantiations coincide:

Analogously for the primed side. By ?, R_1 \Leftrightarrow R_2; set R_T := R_1. By symmetry and transitivity of \mathcal{U}_i through the shared inner-left value, all four goal values are related in \mathcal{U}_i \searrow R_T.

Term part. Compute:

The outer-left and inner-left values coincide as (\ensuremath{\llbracket \sigma \rrbracket(\rho)})(0); the primed pair coincides as (\ensuremath{\llbracket \sigma' \rrbracket(\rho')})(0). By the head clause, (\ensuremath{\llbracket \sigma \rrbracket(\rho)})(0) \approx (\ensuremath{\llbracket \sigma' \rrbracket(\rho')})(0) \in R_T, so all four term values are related in R_T.

Case

Here \Gamma = \Delta, x_0 : U, x = 1{+}y, and T = S[\Uparrow]. Inverting \ensuremath{\vDash \Delta, x_0 : U} gives \ensuremath{\vDash \Delta}, the packaged context PER \Gamma \approx \Gamma \searrow R_\Gamma, and \semtyeq[\Delta]{U}{U}{\ensuremath{\texttt{Ty}_{j}}}.

By ?, \semweak[\Gamma]{\Uparrow}{\Delta}. By ? on \semweak[\Gamma]{\Uparrow}{\Delta} and \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}: \semtyeq[\Gamma']{\Uparrow \circ \sigma}{\Uparrow \circ \sigma'}{\Delta}. By ? on \semweak[\Gamma]{\Uparrow}{\Delta}: \semtyeq[\Gamma]{\Uparrow}{\Uparrow}{\Delta}. From \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} at \Gamma', \ensuremath{\textsf{id}}, \ensuremath{\mathcal{D}}: \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma.

We apply the IH on y : S \in \Delta twice, paralleling the two instantiations used in the Base case.

First IH instantiation. Apply the IH to y : S \in \Delta at \Gamma', the semantic substitution \semtyeq[\Gamma']{\Uparrow \circ \sigma}{\Uparrow \circ \sigma'}{\Delta}, and \ensuremath{\mathcal{D}}: for some R_1,

Second IH instantiation. Apply the IH to y : S \in \Delta at \Gamma (using R_\Gamma), the semantic substitution \semtyeq[\Gamma]{\Uparrow}{\Uparrow}{\Delta}, and \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma: for some R_2,

Match outer values to the goal. By ? (1): = S[\Uparrow \circ \sigma], so the first IH instantiation’s outer-type values are exactly the goal’s outer-type values. The second IH instantiation’s outer-type values \ensuremath{\llbracket S[\Uparrow] \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} are exactly the goal’s inner-type values.

For the term values:

(using (\Uparrow \circ \sigma)(y) = \sigma(y+1) and \ensuremath{\llbracket y[\Uparrow] \rrbracket(\rho_0)} = \ensuremath{\llbracket \Uparrow(y) \rrbracket(\rho_0)} = \rho_0(y+1)). Hence the first IH’s outer-term values equal the goal’s outer-term values, and the second IH’s outer-term values equal the goal’s inner-term values.

Bridge via shared inner. By the identity established in the proof of ?, \ensuremath{\llbracket \Uparrow \circ \sigma \rrbracket(\rho_0)} = (\ensuremath{\llbracket \sigma \rrbracket(\rho_0)})[\Uparrow] for any \rho_0. Also \ensuremath{\llbracket \Uparrow \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} = (\ensuremath{\llbracket \sigma \rrbracket(\rho)})[\Uparrow] by the pointwise definition of weakening evaluation. Hence the inner values of the two IH instantiations coincide:

and analogously for the primed side. By ?, R_1 \Leftrightarrow R_2; set R_T := R_1. By symmetry and transitivity through the shared inner value, all four goal type values are related in \mathcal{U}_i \searrow R_T, and all four goal term values are related in R_T.

By ?, \Gamma \approx \Gamma \searrow R for some R, giving the first premise of the semantic term judgment. Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. By ? on \ensuremath{\vDash \Gamma}, x : T \in \Gamma at this instantiation, the four-value patterns hold for some R_T.

By ?, \Gamma \approx \Gamma \searrow R for some R. Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. We must show

for some R_T, and

Type part. Since \ensuremath{\texttt{Nat}} is closed, all four type values collapse to N:

and analogously for the primed pair.

Term part. Since \textsf{zero} is closed, all four term values collapse to \texttt{ze}:

Since R_T \Leftrightarrow \textsf{Nat}, it suffices to show \texttt{ze} \approx \texttt{ze} \in \textsf{Nat}.

Hence \texttt{ze} \approx \texttt{ze} \in R_T, and the four-value pattern follows.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given.

Type part. Identical to ?: \{\ensuremath{\llbracket \ensuremath{\texttt{Nat}}[\sigma] \rrbracket(\rho)}, \ldots\} \subseteq \mathcal{U}_0 \searrow R_T with R_T \Leftrightarrow \textsf{Nat} by U-Nat.

Term part. We compute the four term values, using that substitution and evaluation distribute over \textsf{su}:

Analogous computations apply to the primed pair, giving \texttt{su}(\ensuremath{\llbracket t' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})}) and \texttt{su}(\ensuremath{\llbracket t'[\sigma'] \rrbracket(\rho')}).

By the hypothesis \semtyeq[\Gamma]{t}{t'}{\ensuremath{\texttt{Nat}}} applied at \Gamma', \sigma \approx \sigma', and \rho \approx \rho' \in R', the term part gives

Applying Nat-Su pointwise (using transitivity of \textsf{Nat}, ?, to chain the four values):

By transitivity of \textsf{Nat}, all four are related in \textsf{Nat}, hence in R_T.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given.

Type part. By ? applied to the hypotheses \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} and \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} (the latter follows from \semtyeq[\Gamma, x:S]{t}{t}{T} via type extraction):

where R is the function PER characterized by: f \approx f' \in R \;\leftrightarrow\; (\forall \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I.\; f \cdot a \approx f' \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I)).

Term part. We compute the four term values using the substitution behavior of \lambda:

Analogously, \ensuremath{\llbracket \lambda x.\,t' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} = \lambda(t',\, \ensuremath{\llbracket \sigma' \rrbracket(\rho')}) and \ensuremath{\llbracket (\lambda x.\,t')[\sigma'] \rrbracket(\rho')} = \lambda(t'[q(\sigma')],\, \rho').

By the biconditional characterization of R, it suffices to show that for every \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I (where R_I is the domain PER), the four closure applications are related in R_O(\ensuremath{\mathcal{D}}_I):

We compute these closure applications:

Analogous identities hold for the primed pair (using t').

By ? on \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}: \semtyeq[\Gamma', x:S[\sigma]]{q(\sigma)}{q(\sigma')}{\Gamma, x:S}. By the first premise of this judgment, (\Gamma', x:S[\sigma]) \approx (\Gamma', x:S[\sigma]) \searrow R_{\Gamma',x:S[\sigma]} and (\Gamma, x:S) \approx (\Gamma, x:S) \searrow R_{\Gamma,x:S}.

By ? on the same left type \ensuremath{\llbracket S[\sigma] \rrbracket(\rho)} governing both R_I (from ?’s domain step) and the head PER R_H' of R_{\Gamma',x:S[\sigma]}, R_I \Leftrightarrow R_H'(\ensuremath{\mathcal{D}}') for \ensuremath{\mathcal{D}}' :: \rho \approx \rho' \in R'. Hence a \approx a' \in R_H'(\ensuremath{\mathcal{D}}'), so by the biconditional of R_{\Gamma',x:S[\sigma]}, (\rho, a/x) \approx (\rho', a'/x) \in R_{\Gamma',x:S[\sigma]}.

Apply the hypothesis \semtyeq[\Gamma, x:S]{t}{t'}{T} at \Gamma', x:S[\sigma], the lifted substitution \semtyeq[\Gamma', x:S[\sigma]]{q(\sigma)}{q(\sigma')}{\Gamma, x:S}, and (\rho, a/x) \approx (\rho', a'/x) \in R_{\Gamma',x:S[\sigma]}:

The outer two values are the closure applications \lambda(t[q(\sigma)], \rho) \cdot a and \lambda(t'[q(\sigma')], \rho') \cdot a'. The inner two values are \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket q(\sigma) \rrbracket((\rho, a/x))})} and \ensuremath{\llbracket t' \rrbracket(\ensuremath{\llbracket q(\sigma') \rrbracket((\rho', a'/x))})}, which we must relate to \ensuremath{\llbracket t \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a/x))} = \lambda(t, \ensuremath{\llbracket \sigma \rrbracket(\rho)}) \cdot a and \ensuremath{\llbracket t' \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))} = \lambda(t', \ensuremath{\llbracket \sigma' \rrbracket(\rho')}) \cdot a'.

We now show \ensuremath{\llbracket q(\sigma) \rrbracket((\rho, a/x))} \approx (\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a/x) \in R_{\Gamma, x:S}. Unfolding q(\sigma) = (\sigma[\Uparrow], x_0/x), the environment \ensuremath{\llbracket q(\sigma) \rrbracket((\rho, a/x))} has tail \ensuremath{\llbracket \sigma[\Uparrow] \rrbracket((\rho, a/x))} and head a (since \ensuremath{\llbracket x_0 \rrbracket((\rho, a/x))} = a). The environment (\ensuremath{\llbracket \sigma \rrbracket(\rho)}, a/x) has tail \ensuremath{\llbracket \sigma \rrbracket(\rho)} and head a. By the biconditional of R_{\Gamma, x:S} (from Ctx-Ext), it suffices to show:

Tails: \ensuremath{\llbracket \sigma[\Uparrow] \rrbracket((\rho, a/x))} \approx \ensuremath{\llbracket \sigma \rrbracket(\rho)} \in R_\Gamma. By ?, \semweak[\Gamma',x:S[\sigma]]{\Uparrow}{\Gamma'}. Apply \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} at \Gamma', x:S[\sigma], \Uparrow, and (\rho, a/x) \approx (\rho', a'/x) \in R_{\Gamma',x:S[\sigma]}: the four-value pattern includes \ensuremath{\llbracket \sigma[\Uparrow] \rrbracket((\rho, a/x))} \approx \ensuremath{\llbracket \sigma \rrbracket(\ensuremath{\llbracket \Uparrow \rrbracket((\rho, a/x))})} \in R_\Gamma. Since \ensuremath{\llbracket \Uparrow \rrbracket((\rho, a/x))} = \rho definitionally (the shift on environments drops the head), this gives the desired relatedness. Let \ensuremath{\mathcal{D}}_\Gamma denote this evidence in R_\Gamma. Heads: a \approx a \in R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma), where R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma) is the head PER governed by \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma[\Uparrow] \rrbracket((\rho, a/x))})} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \in \mathcal{U}_i \searrow R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma). By \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} instantiated at \Gamma', \semtyeq[\Gamma']{\sigma}{\sigma}{\Gamma} (reflexive, by ?, ?), and \rho \approx \rho \in R': the type part gives the commutation \ensuremath{\llbracket S[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \in \mathcal{U}_i. By ?, R_I \Leftrightarrow R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma). From a \approx a \in R_I (reflexive of a \approx a' \in R_I), we conclude a \approx a \in R_H^\Gamma(\ensuremath{\mathcal{D}}_\Gamma).

for some R_O'(\ensuremath{\mathcal{D}}_I). By ?, R_O'(\ensuremath{\mathcal{D}}_I) \Leftrightarrow R_O(\ensuremath{\mathcal{D}}_I) (governed by the same type \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket q(\sigma) \rrbracket((\rho, a/x))})} which lies in \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I) by the type part of the four-value pattern). Analogously on the primed side (using the reflexive instance \semtyeq[\Gamma, x:S]{t'}{t'}{T}): \ensuremath{\llbracket t' \rrbracket(\ensuremath{\llbracket q(\sigma') \rrbracket((\rho', a'/x))})} \approx \ensuremath{\llbracket t' \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))} \in R_O(\ensuremath{\mathcal{D}}_I).

Combining via symmetry and transitivity of R_O(\ensuremath{\mathcal{D}}_I), the four closure applications

Hence the biconditional is satisfied, and the four closures are related in R.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given.

By \semtyeq[\Gamma]{s}{s'}{S} at \Gamma', \sigma \approx \sigma' : \Gamma, \rho \approx \rho' \in R':

In particular, let \ensuremath{\mathcal{D}}_I :: \ensuremath{\llbracket s[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket s'[\sigma'] \rrbracket(\rho')} \in R_I.

By \semtyeq[\Gamma]{r}{r'}{\Pi(x:S).\,T} at the same data, the four evaluations of r, r' are related in the function PER R for \Pi(\ensuremath{\llbracket S[\sigma] \rrbracket(\rho)}, T[q(\sigma)], \rho):

Term part. We compute the four term values:

Analogous computations for the primed pair (with r', s'), yielding \ensuremath{\llbracket r' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \cdot \ensuremath{\llbracket s' \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} and \ensuremath{\llbracket r'[\sigma'] \rrbracket(\rho')} \cdot \ensuremath{\llbracket s'[\sigma'] \rrbracket(\rho')}.

Denote the four r/r'-values as f_1, f_2, f_3, f_4 (in order) and the four s/s'-values as a_1, a_2, a_3, a_4. By hypothesis, \{f_1, f_2, f_3, f_4\} \subseteq R and \{a_1, a_2, a_3, a_4\} \subseteq R_I. For each pair (i, j) with 1 \leq i < j \leq 4, we have f_i \approx f_j \in R and a_i \approx a_j \in R_I; let \ensuremath{\mathcal{D}}_I^{ij} :: a_i \approx a_j \in R_I. By the biconditional of R applied to f_i \approx f_j \in R and \ensuremath{\mathcal{D}}_I^{ij}: f_i \cdot a_i \approx f_j \cdot a_j \in R_O(\ensuremath{\mathcal{D}}_I^{ij}). By ? (right irrelevance), R_O(\ensuremath{\mathcal{D}}_I^{ij}) is independent of the witness, agreeing with R_O(\ensuremath{\mathcal{D}}_I) for any fixed \ensuremath{\mathcal{D}}_I :: a_1 \approx a_4 \in R_I. Hence

Type part. We instantiate \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at two semantic substitutions to obtain the goal’s outer and inner values, then bridge via ?.

Pattern A (outer instantiation): (\sigma, s[\sigma]/x) vs (\sigma', s'[\sigma']/x).

Apply \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', this semantic substitution, and \rho \approx \rho' \in R':

Identify the four values syntactically and definitionally:

Hence the four-value pattern reads:

The outer-left value matches the goal’s outer-left \ensuremath{\llbracket \rrbracket(\rho)}. The outer-right value \ensuremath{\llbracket \rrbracket(\rho')} governs the same PER as \ensuremath{\llbracket \rrbracket(\rho')} by ? once we establish

which holds by another instantiation of \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at the related env-pair

(using the four-value relatedness of s, s').

Pattern B (inner instantiation): (\ensuremath{\textsf{id}}, s/x) vs (\ensuremath{\textsf{id}}, s'/x). By ? on \semtyeq[\Gamma]{\ensuremath{\textsf{id}}}{\ensuremath{\textsf{id}}}{\Gamma} and \semtyeq[\Gamma]{s}{s'}{S}: \semtyeq[\Gamma]{(\ensuremath{\textsf{id}}, s/x)}{(\ensuremath{\textsf{id}}, s'/x)}{\Gamma, x:S} (using s[\ensuremath{\textsf{id}}] = s and s'[\ensuremath{\textsf{id}}] = s'). From \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} at \ensuremath{\textsf{id}}, \ensuremath{\mathcal{D}}: \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma. Apply \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma (with R_\Gamma), this semantic substitution, and \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma:

Identify T[\ensuremath{\textsf{id}}, s/x] = T[s/x], T[\ensuremath{\textsf{id}}, s'/x] = T[s'/x], and \ensuremath{\llbracket (\ensuremath{\textsf{id}}, s/x) \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} = (\ensuremath{\llbracket \sigma \rrbracket(\rho)}, \ensuremath{\llbracket s \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})}/x) (pointwise; \ensuremath{\llbracket \ensuremath{\textsf{id}} \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} = \ensuremath{\llbracket \sigma \rrbracket(\rho)}). So the four-value pattern reads:

The outer values match the goal’s inner-left \ensuremath{\llbracket T[s/x] \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} and inner-right \ensuremath{\llbracket T[s'/x] \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} (modulo ? on T[s/x] vs T[s'/x] at \ensuremath{\llbracket \sigma' \rrbracket(\rho')}, established as in Pattern A).

Bridging Pattern A and Pattern B. Pattern A’s inner-left is

and Pattern B’s inner-left is

We bridge them via ?. We show

by Ctx-Ext’s biconditional:

Apply ? on \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at this related pair:

Analogously on the primed side, bridging Pattern A’s inner-right and Pattern B’s inner-right:

Combining. By transitivity of \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I) through the bridges:

Hence the goal’s outer-left \approx goal’s inner-left in \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I). Analogously for outer-right \approx inner-right (using the primed bridge). Combined with Pattern A’s outer pair and Pattern B’s outer pair (which directly relate inner-left to inner-right in their respective four-value patterns), all four type values lie pairwise in \mathcal{U}_i \searrow R_O(\ensuremath{\mathcal{D}}_I).

We first establish the second claim.

for some R_T.

We prove the first claim by induction on a \approx a' \in \textsf{Nat}.

Case

Here a = a' = \texttt{ze}.

We must show b \approx b' \in R_T.

Hence b \approx b' \in R_z. We show R_z \Leftrightarrow R_T.

Hence b \approx b' \in R_T.

Case

with a = \texttt{su}(a_0), a' = \texttt{su}(a_0'). By IH on a_0 \approx a_0', there exist b_0, b_0' with

By rec-su:

We must show b \approx b' \in R_T. Build the env-pair in R_{\Gamma, x:\ensuremath{\texttt{Nat}}, y:T}:

Apply ? on \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s}{s'} {T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} at this env-pair:

where R_s is the PER governed by

Hence b \approx b' \in R_s.

We show R_s \Leftrightarrow R_T by instantiating hypothesis on T at the substitution \tau := (\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x) over \Gamma, x:\ensuremath{\texttt{Nat}}, y:T (mapping into \Gamma, x:\ensuremath{\texttt{Nat}}). Semantic well-formedness of \tau:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma, x:\ensuremath{\texttt{Nat}}, y:T, \tau \approx \tau, and the env-pair (\rho, a_0/x, b_0/y) \approx (\rho, a_0/x, b_0/y) \in R_{\Gamma, x:\ensuremath{\texttt{Nat}}, y:T} (reflexive):

Hence:

Combining with the second claim \ensuremath{\llbracket T \rrbracket((\rho, \texttt{su}(a_0)/x))} \approx \ensuremath{\llbracket T \rrbracket((\rho', \texttt{su}(a_0')/x))} \in \mathcal{U}_i \searrow R_T (applied at \texttt{su}(a_0) \approx \texttt{su}(a_0')):

Hence b \approx b' \in R_T.

Case

with a = {\uparrow}^N(e), a' = {\uparrow}^N(e'). Compute the eliminator outputs by rec-ne:

We must show b \approx b' \in R_T. By ? on A \approx A' \in \mathcal{U}_i \searrow R_T, it suffices to show

i.e. for every depth n both sides read back via \textsf{R}^{\textsf{Ne}}_n to the same neutral normal form. By rule Re-rec:

whenever

(and analogously for the primed side, producing \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,W_T')~w_z'~(x, y.\,w_s')~u'}). We show each component reads back to the same syntactic form.

Motive W_T = W_T'. Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at the env-pair extended with the fresh level \ell_n:

Zero branch w_z = w_z'. Apply \semtyeq[\Gamma]{z}{z'}{T[\textsf{zero}/x]} at \Gamma, \ensuremath{\textsf{id}}, and \rho \approx \rho' \in R_\Gamma (term and type parts):

Bridge R_z \Leftrightarrow R_T-at-\texttt{ze} via the same outer-vs-inner pattern as the Nat-Ze case (instantiate T at (\ensuremath{\textsf{id}}, \textsf{zero}/x)). By ? on a_z \approx a_z' \in R_T-at-\texttt{ze}:

Step branch w_s = w_s'. Build the env-pair at fresh levels:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s}{s'}{T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} at this env-pair (term and type parts, after bridging T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x] to T at \texttt{su}({\uparrow}^N(\ell_n))/x as in the Nat-Su case):

By ?:

Underlying neutral u = u'. By hypothesis e \approx e' \in \textsf{Ne}:

Combining:

Hence b \approx b' \in R_T.

We first establish the lifted substitution and the second claim.

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T'}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', x:\ensuremath{\texttt{Nat}}, the lifted substitution, and the env-pair above:

Bridge \ensuremath{\llbracket q(\sigma') \rrbracket((\rho', a'/x))} to (\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x):

By transitivity of \mathcal{U}_i and ?, \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, a/x))} \approx \ensuremath{\llbracket T' \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))} \in \mathcal{U}_i \searrow R_T, establishing the second claim.

We prove the first claim by induction on a \approx a' \in \textsf{Nat}.

Case

Here a = a' = \texttt{ze}. Apply \semtyeq[\Gamma]{z}{z'}{T[\textsf{zero}/x]} at \Gamma', \sigma \approx \sigma', and \rho \approx \rho' \in R' (this gives the four-value pattern of z, z'):

Then by rec-ze applied to these evaluations:

We must show b \approx b' \in R_T. Currently b \approx b' \in R_z where R_z is governed by \ensuremath{\llbracket \rrbracket(\rho)}, while R_T is governed by \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, \texttt{ze}/x))} (substituted left, second-claim instance at a = a' = \texttt{ze}). We bridge R_z \Leftrightarrow R_T via two type-hypothesis instantiations.

Left bridge. By ? on \semtyeq[\Gamma']{\sigma}{\sigma}{\Gamma} (reflexive instance via ?, ?) and \semtyeq[\Gamma']{\textsf{zero}[\sigma]}{\textsf{zero}[\sigma]}{\ensuremath{\texttt{Nat}}[\sigma]} (using \textsf{zero}[\sigma] = \textsf{zero}, \ensuremath{\texttt{Nat}}[\sigma] = \ensuremath{\texttt{Nat}}, and ?):

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', this substitution, and \rho \approx \rho \in R' (reflexive):

Hence \ensuremath{\llbracket \rrbracket(\rho)} \approx \ensuremath{\llbracket T \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, \texttt{ze}/x))} \in \mathcal{U}_i \searrow R_z.

Right bridge. Symmetrically, instantiate T at (\ensuremath{\textsf{id}}, \textsf{zero}/x) over \Gamma at the env-pair \ensuremath{\llbracket \sigma \rrbracket(\rho)} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma (carried by the semantic-substitution hypothesis):

Combining via the second claim. The second claim (proved above) gives:

Chaining via the bridges (using ?, ?, ?):

Hence b \approx b' \in R_T.

Case

with a = \texttt{su}(a_0), a' = \texttt{su}(a_0'). By IH on a_0 \approx a_0', there exist b_0, b_0' with

We derive the evaluations of s[q^2(\sigma)] and s' from the hypothesis on s, s'. First, lift \sigma, \sigma' over \ensuremath{\texttt{Nat}} and T:

Build the env-pair via two applications of Ctx-Ext:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s}{s'}{T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} at \Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)], the doubly-lifted substitution q^2(\sigma) \approx q^2(\sigma'), and this env-pair (this gives the four-value pattern of s, s'):

By rec-su:

We must show b \approx b' \in R_T. Outer-left vs inner-right of the four-value pattern of s, s':

where R_s is the PER governed by \ensuremath{\llbracket (T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x])[q^2(\sigma)] \rrbracket((\rho, a_0/x, b_0/y))}. Bridge \ensuremath{\llbracket q^2(\sigma') \rrbracket((\rho', a_0'/x, b_0'/y))} to (\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a_0'/x, b_0'/y) in R_{\Gamma, x:\ensuremath{\texttt{Nat}}, y:T} analogously, then apply ? on \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s'}{s'}{T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} (the reflexive instance):

By transitivity, b \approx b' \in R_s.

We bridge R_s \Leftrightarrow R_T, where R_s is governed by \ensuremath{\llbracket (T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x])[q^2(\sigma)] \rrbracket((\rho, a_0/x, b_0/y))} and R_T is governed by \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, \texttt{su}(a_0)/x))} (the second-claim pattern instantiated at \texttt{su}(a_0) \approx \texttt{su}(a_0')):

All bridging uses syntactic substitution-composition lemmas (?, ?, ?) and instantiations of hypothesis on T.

Bridge B1: collapse (T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x])[q^2(\sigma)] into a single substitution.

Denote the collapsed substitution by \tau := (\sigma \circ (\Uparrow \circ \Uparrow),\, \textsf{succ}~x_1/x), with \judge[\Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)]]{\tau : \Gamma, x:\ensuremath{\texttt{Nat}}}.

Bridge B2: instantiate hypothesis on T via \tau. We show \tau is a semantic substitution from \Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)] to \Gamma, x:\ensuremath{\texttt{Nat}}. By ? (twice) and ?: \semweak[\Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)]]{\Uparrow \circ \Uparrow}{\Gamma'}. Apply ? to \semtyeq[\Gamma']{\sigma}{\sigma}{\Gamma} (reflexive, by ?, ?) and this semantic weakening:

By ?, ?: \semtyeq[\Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)]] {\textsf{succ}~x_1}{\textsf{succ}~x_1}{\ensuremath{\texttt{Nat}}} (lookup x_1 : \ensuremath{\texttt{Nat}} at the second slot of \Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)], with \ensuremath{\texttt{Nat}}[\Uparrow] = \ensuremath{\texttt{Nat}}). By ?:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)], \tau \approx \tau, and the reflexive env-pair (\rho, a_0/x, b_0/y) \approx (\rho, a_0/x, b_0/y) \in R_{\Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)]}. Outer-left vs inner-left:

By Bridge B1,

so the outer-left is exactly

— the value governing R_s. Hence R_s \Leftrightarrow R_{B2}.

By pointwise definition of substitution evaluation:

We do not equate the tail \ensuremath{\llbracket \sigma \circ (\Uparrow \circ \Uparrow) \rrbracket((\rho, a_0/x, b_0/y))} with \ensuremath{\llbracket \sigma \rrbracket(\rho)} definitionally — such an equality is a substitution–evaluation commutation that does not hold for operational substitutions. Instead, we relate them in R_\Gamma via the four-value pattern of \sigma \circ (\Uparrow \circ \Uparrow) := \sigma[\Uparrow \circ \Uparrow] established by ?, and the four-value pattern of \sigma itself:

By transitivity of R_\Gamma:

Bridge B3: instantiate hypothesis on T via q(\sigma). Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', x:\ensuremath{\texttt{Nat}}, the lifted q(\sigma) \approx q(\sigma), and reflexive (\rho, \texttt{su}(a_0)/x) \approx (\rho, \texttt{su}(a_0)/x) \in R_{\Gamma', x:\ensuremath{\texttt{Nat}}} (head \texttt{su}(a_0) \approx \texttt{su}(a_0) via ? reflexivity). Outer-left vs inner-left:

Combining B2 and B3. By B2’s bridging, \ensuremath{\llbracket \tau \rrbracket((\rho, a_0/x, b_0/y))} \approx (\ensuremath{\llbracket \sigma \rrbracket(\rho)}, \texttt{su}(a_0)/x) \in R_{\Gamma, x:\ensuremath{\texttt{Nat}}}. By B3’s Ctx-Ext computation, \ensuremath{\llbracket q(\sigma) \rrbracket((\rho, \texttt{su}(a_0)/x))} \approx (\ensuremath{\llbracket \sigma \rrbracket(\rho)}, \texttt{su}(a_0)/x) \in R_{\Gamma, x:\ensuremath{\texttt{Nat}}} (PER-related, via the lifted-substitution evidence). Apply ? on T to bridge the B3 inner-left:

Both B2 and B3 inner-left values are now \mathcal{U}_i-related to the common value \ensuremath{\llbracket T \rrbracket((\ensuremath{\llbracket \sigma \rrbracket(\rho)}, \texttt{su}(a_0)/x))}, so by transitivity and ?, R_{B2} \Leftrightarrow R_{B3}.

Chaining: R_s \Leftrightarrow R_{B2} \Leftrightarrow R_{B3} \Leftrightarrow R_T. Hence b \approx b' \in R_T.

Case

with a = {\uparrow}^N(e), a' = {\uparrow}^N(e'). Compute the eliminator outputs by rec-ne:

We must show b \approx b' \in R_T. By ? on A \approx A' \in \mathcal{U}_i \searrow R_T, it suffices to show

i.e. for every depth n both sides read back via \textsf{R}^{\textsf{Ne}}_n to the same neutral normal form. By rule Re-rec:

whenever

and analogously for the primed side, producing \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,W_T')~w_z'~(x, y.\,w_s')~u'}. We show each component reads back to the same syntactic form.

Motive W_T = W_T'. Apply the second claim of this lemma at the fresh-level relation {\uparrow}^N(\ell_n) \approx {\uparrow}^N(\ell_n) \in \textsf{Nat} (by Nat-Ne, \ell_n \approx \ell_n \in \textsf{Ne}):

No separate env-pair construction is needed: the second claim is parametric in a \approx a' \in \textsf{Nat} and directly relates the two motive values at envs over the heterogeneous source–target contexts.

Zero branch w_z = w_z'. By the Nat-Ze sub-case proved above, a_z \approx a_z' \in R_T-at-\texttt{ze} (the PER governed by \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, \texttt{ze}/x))}, which equals A_z). By ?:

Step branch w_s = w_s'. We obtain b_s \approx b_s' at fresh levels by replaying the Nat-Su case with a_0 := {\uparrow}^N(\ell_n). First, lift \sigma, \sigma' to handle the binders of s:

Build the env-pair via two applications of Ctx-Ext:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s}{s'}{T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} at \Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)], the doubly-lifted substitution q^2(\sigma) \approx q^2(\sigma'), and this env-pair. The four-value pattern of s, s' gives:

where R_T^{step} is governed by \ensuremath{\llbracket (T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x])[q^2(\sigma)] \rrbracket((\rho, {\uparrow}^N(\ell_n)/x, {\uparrow}^{A_x}(\ell_{n+1})/y))}.

By the B1/B2/B3 bridging of the Nat-Su case (with a_0 replaced by {\uparrow}^N(\ell_n)):

i.e. the PER at \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, \texttt{su}({\uparrow}^N(\ell_n))/x))}, which equals A_x^{\textsf{succ}~}. Hence b_s \approx b_s' \in R_T^\ell-at-\texttt{su}(\ell_n), and:

Underlying neutral u = u'. By hypothesis e \approx e' \in \textsf{Ne}:

Combining:

Hence b \approx b' \in R_T.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. Write \rho_\sigma := \ensuremath{\llbracket \sigma \rrbracket(\rho)} and \rho_{\sigma'} := \ensuremath{\llbracket \sigma' \rrbracket(\rho')}. From \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} at \ensuremath{\textsf{id}}, \ensuremath{\mathcal{D}}: \rho_\sigma \approx \rho_{\sigma'} \in R_\Gamma where \Gamma \approx \Gamma \searrow R_\Gamma.

By \semtyeq[\Gamma]{t}{t'}{\ensuremath{\texttt{Nat}}} applied at \Gamma', \sigma \approx \sigma', \rho \approx \rho' \in R':

Compute the four eliminator term values:

Analogous computations for the primed pair (using z', s', t'): \mathsf{rec}(\ensuremath{\llbracket t'[\sigma'] \rrbracket(\rho')},\, T[q(\sigma')],\, z'[\sigma'],\, s'[q^2(\sigma')],\, \rho') and \mathsf{rec}(\ensuremath{\llbracket t' \rrbracket(\rho_{\sigma'})},\, T,\, z',\, s',\, \rho_{\sigma'}).

Before applying the helpers, derive reflexive instances of all hypotheses (the helpers’ RHS are in primed form; we sometimes need unprimed-to-unprimed instances):

(Primed analogues hold symmetrically.)

Inner pair via the unsubstituted helper. Apply ? at T \approx T (reflexive), z \approx z', s \approx s', R_\Gamma, env-pair \rho_\sigma \approx \rho_{\sigma'}, and witness \ensuremath{\llbracket t \rrbracket(\rho_\sigma)} \approx \ensuremath{\llbracket t' \rrbracket(\rho_{\sigma'})} \in \textsf{Nat} (inner-left vs inner-right of the four-value pattern of t, t'):

where R_T is governed by \ensuremath{\llbracket T \rrbracket((\rho_\sigma, \ensuremath{\llbracket t \rrbracket(\rho_\sigma)}/x))} \approx \ensuremath{\llbracket T \rrbracket((\rho_{\sigma'}, \ensuremath{\llbracket t' \rrbracket(\rho_{\sigma'})}/x))} \in \mathcal{U}_i \searrow R_T. These match the goal’s inner-left and inner-right term values.

Outer-vs-inner via the one-sided helper. Apply ? at T \approx T, z \approx z, s \approx s (all reflexive), \Gamma' \approx \Gamma' \searrow R', \sigma \approx \sigma (reflexive), \rho \approx \rho \in R' (reflexive), and witness \ensuremath{\llbracket t[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket t \rrbracket(\rho_\sigma)} \in \textsf{Nat} (outer-left vs inner-left of the four-value pattern of t):

where R_T^{oi} is governed by \ensuremath{\llbracket T[q(\sigma)] \rrbracket((\rho, \ensuremath{\llbracket t[\sigma] \rrbracket(\rho)}/x))} \approx \ensuremath{\llbracket T \rrbracket((\rho_\sigma, \ensuremath{\llbracket t \rrbracket(\rho_\sigma)}/x))} \in \mathcal{U}_i \searrow R_T^{oi}. By ?, R_T^{oi} \Leftrightarrow R_T. Hence b_o \approx b_i \in R_T.

Apply ? symmetrically at the primed reflexive instances (T' \approx T', z' \approx z', s' \approx s', \sigma' \approx \sigma', \rho' \approx \rho' \in R'), with witness \ensuremath{\llbracket t'[\sigma'] \rrbracket(\rho')} \approx \ensuremath{\llbracket t' \rrbracket(\rho_{\sigma'})} \in \textsf{Nat}:

Combining. We assemble the four goal term values:

Thus all four goal term values \{b_o, b_i, b_i', b_o'\} are pairwise related in R_T.

Type part. The goal type is T[t/x] on the LHS and T[t'/x] on the RHS (by the syntactic conclusion’s type, via the four-value pattern of the outer \semtyeq[\Gamma]{\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(\ldots)~\ldots~(\ldots)~t}}{\ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(\ldots)~\ldots~(\ldots)~t'}}{T[t/x]} semantic judgment). We bridge the four goal type values via outer and inner instantiations of T \approx T'.

Outer instantiation. By ? on \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \semtyeq[\Gamma]{t}{t'}{\ensuremath{\texttt{Nat}}}:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T'}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma', this semantic substitution, and \rho \approx \rho' \in R':

Now the goal’s outer-RHS type is \ensuremath{\llbracket \rrbracket(\rho')}, but the outer instantiation gives \ensuremath{\llbracket (T'[t'/x])[\sigma'] \rrbracket(\rho')}. We show these coincide modulo \mathcal{U}_i:

So the four values lie in \mathcal{U}_i \searrow R_T^{out} with the outer-LHS value exactly matching the goal’s \ensuremath{\llbracket \rrbracket(\rho)} and the outer-RHS value matching the goal’s \ensuremath{\llbracket \rrbracket(\rho')} (modulo \mathcal{U}_i, hence by ?).

Inner instantiation. By ? over \Gamma on \semtyeq[\Gamma]{\ensuremath{\textsf{id}}}{\ensuremath{\textsf{id}}}{\Gamma} and \semtyeq[\Gamma]{t}{t'}{\ensuremath{\texttt{Nat}}}:

Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T'}{\ensuremath{\texttt{Ty}_{i}}} at \Gamma, this semantic substitution, and \rho_\sigma \approx \rho_{\sigma'} \in R_\Gamma:

Bridging. The inner-pair values \ensuremath{\llbracket T \rrbracket((\rho_\sigma, \ensuremath{\llbracket t \rrbracket(\rho_\sigma)}/x))} (shared between outer and inner instantiations) and \ensuremath{\llbracket T' \rrbracket((\rho_{\sigma'}, \ensuremath{\llbracket t' \rrbracket(\rho_{\sigma'})}/x))} (shared) bridge the PERs:

Hence all four goal type values lie in \mathcal{U}_i \searrow R_T, with the term values \{b_o, b_i, b_i', b_o'\} in R_T as established.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given.

Type part. By \semtyeq[\Gamma]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at the given data:

Term part. By \semtyeq[\Gamma]{t}{t}{S} at the given data:

By \Gamma \vDash S \subseteq T at the given data:

By ? applied to the subtyping \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \mathrel{<:_i} \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} together with \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \approx \ensuremath{\llbracket S \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \in \mathcal{U}_i \searrow R_S and \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \approx \ensuremath{\llbracket T \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \in \mathcal{U}_i \searrow R_T:

Hence the four term values, which lie in R_S, also lie in R_T:

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given.

LHS computation at \sigma, \rho. By the syntactic action of substitution on \lambda and application, then ev-app/ev-lam/closure-application:

RHS expression at \sigma, \rho. Using the sugar [s/x] = [\ensuremath{\textsf{id}}, s/x] and ?, ?:

Let b_R satisfy \ensuremath{\llbracket t[\sigma, s[\sigma]/x] \rrbracket(\rho)} \searrow b_R (existence via the four-value pattern below). We relate b_L and b_R in the term PER via the four-value pattern of t on the extended substitution.

Relatedness. By ? on \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \semtyeq[\Gamma]{s}{s}{S}:

Apply \semtyeq[\Gamma, x:S]{t}{t}{T} at \Gamma', this extended substitution, and \rho \approx \rho' \in R'. Let R_T be the PER governing the four-value pattern of t at this instantiation; concretely, R_T is determined by the type four-value pattern of T at the same env-pair (carried by semantic typing of t : T):

The term four-value pattern then gives:

By the syntactic identity above (and analogously at \sigma', \rho'), the outer values coincide with the goal’s RHS outer-values \{\ensuremath{\llbracket \rrbracket(\rho)}, \ensuremath{\llbracket \rrbracket(\rho')}\}.

LHS values via four-value pattern of t at q(\sigma). We bridge b_L = \ensuremath{\llbracket t[q(\sigma)] \rrbracket((\rho, a_s/x))} to the inner-left value \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket (\sigma, s[\sigma]/x) \rrbracket(\rho)})} above. By ? on \semtyeq[\Gamma']{\sigma}{\sigma}{\Gamma} (reflexive, via ?, ?) and \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}}:

The reflexive env-pair (\rho, a_s/x) \approx (\rho, a_s/x) in R_{\Gamma', x:S[\sigma]} holds via Ctx-Ext (head a_s \approx a_s reflexively in the head PER, tail \rho \approx \rho \in R'). Apply \semtyeq[\Gamma, x:S]{t}{t}{T} at \Gamma', x:S[\sigma], q(\sigma) \approx q(\sigma), and this env-pair (four-value pattern of t, outer-left vs inner-left):

Bridge \ensuremath{\llbracket q(\sigma) \rrbracket((\rho, a_s/x))} to \ensuremath{\llbracket (\sigma, s[\sigma]/x) \rrbracket(\rho)} in R_{\Gamma, x:S} pointwise. Both envs have head a_s:

Apply ? on the reflexive instance \semtyeq[\Gamma, x:S]{t}{t}{T} at this env-pair:

By transitivity, b_L \approx \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket (\sigma, s[\sigma]/x) \rrbracket(\rho)})} in R_T (the inner-left value of the relatedness pattern). Symmetrically for the primed side.

Combining: all eight values (four LHS, four RHS) lie in R_T, so the LHS-RHS pair at each of the four positions is in R_T.

Type part. Already established: the type four-value pattern displayed above (in \mathcal{U}_i \searrow R_T) is the goal’s T[s/x] pattern, since T[\sigma, s[\sigma]/x] = by the syntactic identity used for the term part.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given.

LHS values. By \semtyeq[\Gamma]{t}{t}{\Pi(x:S).\,T} at \Gamma', \sigma \approx \sigma', \rho \approx \rho' \in R', the four evaluations of t are related in the function PER R:

with biconditional characterization f \approx f' \in R \;\leftrightarrow\; (\forall \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I.\; f \cdot a \approx f' \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I)).

RHS values. The RHS evaluates on the \sigma', \rho'-side only:

where f_o := \lambda(t[\Uparrow][q(\sigma')]\;x,\, \rho') and f_i := \lambda(t[\Uparrow]\;x,\, \ensuremath{\llbracket \sigma' \rrbracket(\rho')}).

Step 1: \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \approx f_o in R. By the biconditional, suffices to show: for every \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I, \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \cdot a \approx f_o \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I).

Compute f_o \cdot a':

Bridge \ensuremath{\llbracket t[\sigma'[\Uparrow]] \rrbracket((\rho', a'/x))} \approx \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \in R:

Apply hypothesis on t at \Gamma', x:S[\sigma'], \sigma'[\Uparrow] \approx \sigma'[\Uparrow], env-pair (\rho', a'/x) \approx (\rho', a'/x) \in R_{\Gamma', x:S[\sigma']}:

Apply hypothesis on \sigma' at the same data (\Uparrow as the weakening, env-pair as above), giving \ensuremath{\llbracket \sigma'[\Uparrow] \rrbracket((\rho', a'/x))} \approx \ensuremath{\llbracket \sigma' \rrbracket(\rho')} \in R_\Gamma (using \ensuremath{\llbracket \Uparrow \rrbracket((\rho', a'/x))} = \rho' pointwise). By ? on t:

Chained with \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \approx \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \in R (four-value pattern of t, inner-left vs outer-left):

Apply the biconditional of R at \ensuremath{\mathcal{D}}_I: \ensuremath{\llbracket t[\sigma'[\Uparrow]] \rrbracket((\rho', a'/x))} \cdot a \approx \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I). Since f_o \cdot a' = \ensuremath{\llbracket t[\sigma'[\Uparrow]] \rrbracket((\rho', a'/x))} \cdot a', by symmetry of R_O on the reflexive instance of \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \approx \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \in R at a \approx a': \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \cdot a \approx f_o \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I).

Step 2: \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \approx f_i in R. Suffices to show: for every \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I, \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \cdot a \approx f_i \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I).

Compute:

Bridge \ensuremath{\llbracket t[\Uparrow] \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))} \approx \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \in R via the four-value pattern of t (reflexive) at the new context \Gamma, x:S, \semweak[\Gamma, x:S]{\Uparrow}{\Gamma}, env-pair (\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x) \approx (\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x) \in R_{\Gamma, x:S}: outer-left \ensuremath{\llbracket t[\Uparrow] \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))}, inner-left \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \Uparrow \rrbracket((\ensuremath{\llbracket \sigma' \rrbracket(\rho')}, a'/x))})} = \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} (pointwise). Apply biconditional at \ensuremath{\mathcal{D}}_I and the reflexive \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \approx \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} at a \approx a': \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \cdot a \approx f_i \cdot a' \in R_O(\ensuremath{\mathcal{D}}_I).

Combining. By the four-value pattern of t, all four LHS values are pairwise related in R. By Steps 1 and 2, \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')} \approx f_o and \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma' \rrbracket(\rho')})} \approx f_i in R. By symmetry and transitivity of R, every LHS-RHS pair (e.g. \ensuremath{\llbracket t[\sigma] \rrbracket(\rho)} \approx f_o, \ensuremath{\llbracket t \rrbracket(\ensuremath{\llbracket \sigma \rrbracket(\rho)})} \approx f_i, etc.) lies in R.

Type part. By ? on \semtyeq[\Gamma]{S}{S}{\ensuremath{\texttt{Ty}_{i}}} and \semtyeq[\Gamma, x:S]{T}{T}{\ensuremath{\texttt{Ty}_{i}}}, the four-value pattern of \Pi(x:S).\,T in \mathcal{U}_i is established. The goal’s type is \Pi(x:S).\,T on both sides, exactly this pattern.

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. Write \rho_\sigma := \ensuremath{\llbracket \sigma \rrbracket(\rho)} and \rho_{\sigma'} := \ensuremath{\llbracket \sigma' \rrbracket(\rho')}.

LHS computation on the \sigma, \rho- and \rho_\sigma-side. The LHS is \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x, y.\, s)~\textsf{zero}}. Outer-LHS at \sigma, \rho:

Inner-LHS at \rho_\sigma:

RHS values on the \sigma', \rho'- and \rho_{\sigma'}-side. The RHS is z, evaluated directly:

Relatedness. By \semtyeq[\Gamma]{z}{z}{T[\textsf{zero}/x]} at \Gamma', \sigma \approx \sigma', \rho \approx \rho' \in R' (four-value pattern of z):

where R_z is the PER governed by the type four-value pattern of T[\textsf{zero}/x]. The LHS values b, b' coincide with \ensuremath{\llbracket z[\sigma] \rrbracket(\rho)} and \ensuremath{\llbracket z \rrbracket(\rho_\sigma)} (the unprimed-side outer-LHS and inner-LHS of the z pattern). The RHS values \ensuremath{\llbracket z[\sigma'] \rrbracket(\rho')} and \ensuremath{\llbracket z \rrbracket(\rho_{\sigma'})} are exactly the primed-side outer-RHS and inner-RHS of the same pattern. Hence all four LHS-RHS pairs lie in R_z.

Bridge R_z \Leftrightarrow R_T (where R_T is the goal’s type PER, governed by \ensuremath{\llbracket T[\textsf{zero}/x][\sigma] \rrbracket(\rho)}): the goal’s type is also T[\textsf{zero}/x], so R_z = R_T (functionality of \mathcal{U}_i, ?).

Let \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. Write \rho_\sigma := \ensuremath{\llbracket \sigma \rrbracket(\rho)} and \rho_{\sigma'} := \ensuremath{\llbracket \sigma' \rrbracket(\rho')}. Let a = \ensuremath{\llbracket t \rrbracket(\rho_\sigma)}, a' = \ensuremath{\llbracket t \rrbracket(\rho_{\sigma'})}, b_t = \ensuremath{\llbracket t[\sigma] \rrbracket(\rho)}, b_{t'} = \ensuremath{\llbracket t[\sigma'] \rrbracket(\rho')}.

Denote E := \ensuremath{\textsf{elim}_{\ensuremath{\texttt{Nat}}}~(x.\,T)~z~(x, y.\, s)~t} (the inner eliminator with scrutinee t; this is the recursive call appearing in the \beta-su rule). Define c_t := \ensuremath{\llbracket E[\sigma] \rrbracket(\rho)}, c_{t'} := \ensuremath{\llbracket E[\sigma'] \rrbracket(\rho')}, c := \ensuremath{\llbracket E \rrbracket(\rho_\sigma)}, c' := \ensuremath{\llbracket E \rrbracket(\rho_{\sigma'})} (the four evaluations of E at the corresponding positions; existence by termination of evaluation).

LHS computation. By the syntactic action of substitution on \textsf{elim}_{\ensuremath{\texttt{Nat}}}, ev-rec, and rec-su:

At the inner position:

RHS expression on the \sigma', \rho'-side. The RHS appears on the right of \approx in the goal, so the four-value pattern’s RHS values are \ensuremath{\llbracket \rrbracket(\rho')} (outer-RHS) and \ensuremath{\llbracket s[t/x, E/y] \rrbracket(\rho_{\sigma'})} (inner-RHS). By ?, ?, ?:

Doubly-extended semantic substitution. We need the recursive call to be semantically valid: by ?, \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{x}{x}{\ensuremath{\texttt{Nat}}}. By ? on T \approx T, z \approx z, s \approx s (all reflexive hypotheses, using ?, ?) and x \approx x:

By ? on \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, \semtyeq[\Gamma]{t}{t}{\ensuremath{\texttt{Nat}}}, and the above (with the head substitution computing E[\sigma] on the LHS, E[\sigma'] on the RHS):

Four-value pattern of s at the doubly-extended substitution. Apply \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s}{s}{T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} at the above substitution and \rho \approx \rho' \in R':

By substitution-extension evaluation:

where c_{t'} is the corresponding recursive-call value. Hence the four values of the pattern read:

Identifying R_O. R_O is the PER returned by the type four-value pattern of T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x] at the same doubly-extended substitution. We bridge it to the PER at \ensuremath{\llbracket T \rrbracket((\rho_\sigma, \texttt{su}(a)/x))} (which is the goal’s type T[\textsf{succ}~t/x] evaluated at the inner position) via two steps.

Step (a): collapse the iterated substitution. Denote \tau_* := (\sigma, t[\sigma]/x, E[\sigma]/y) (the doubly-extended substitution from \Gamma' to \Gamma, x:\ensuremath{\texttt{Nat}}, y:T). The value \ensuremath{\llbracket (T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x])[\tau_*] \rrbracket(\rho)} governs R_O. By ? and ?:

Hence the collapsed substitution is (\sigma,\, \textsf{succ}~t[\sigma]/x):

Step (b): instantiate hypothesis on T at the collapsed substitution. By the IH on \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}]{T}{T}{\ensuremath{\texttt{Ty}_{i}}}, applied at \Gamma', the semantic substitution \semtyeq[\Gamma']{(\sigma, \textsf{succ}~t[\sigma]/x)}{(\sigma', \textsf{succ}~t[\sigma']/x)}{\Gamma, x:\ensuremath{\texttt{Nat}}} (by ? on \sigma \approx \sigma' and \textsf{succ}~t[\sigma] \approx \textsf{succ}~t[\sigma'] \in \textsf{Nat} via Nat-Su on the t-pattern), and \rho \approx \rho' \in R':

Bridge \texttt{su}(b_t) to \texttt{su}(a): from the four-value pattern of t,

(outer-LHS vs inner-LHS), so \texttt{su}(b_t) \approx \texttt{su}(a) \in \textsf{Nat} by Nat-Su. By ? on T:

By transitivity and ?, R_O is the PER at \ensuremath{\llbracket T \rrbracket((\rho_\sigma, \texttt{su}(a)/x))} — the goal’s type T[\textsf{succ}~t/x] inner-LHS value (since T[\textsf{succ}~t/x] evaluated at \rho_\sigma equals T at the inner-extended env, modulo the same bridge).

LHS-RHS bridging. The RHS outer-RHS value is \ensuremath{\llbracket \rrbracket(\rho')} = \ensuremath{\llbracket s[\sigma', t[\sigma']/x, E[\sigma']/y] \rrbracket(\rho')}, which is the outer-RHS of the four-value pattern of s above. Similarly, the RHS inner-RHS value \ensuremath{\llbracket s[t/x, E/y] \rrbracket(\rho_{\sigma'})} relates to \ensuremath{\llbracket s \rrbracket((\rho_{\sigma'}, b_{t'}/x, c_{t'}/y))} via the four-value pattern of s on the primed side (analogous to the LHS-side bridging below).

For LHS values (the \sigma, \rho- and \rho_\sigma-sides of the goal): the LHS computation gives b_L = \ensuremath{\llbracket s[q^2(\sigma)] \rrbracket((\rho, b_t/x, c_t/y))} at \sigma, \rho, and b_I = \ensuremath{\llbracket s \rrbracket((\rho_\sigma, a/x, c/y))} at \rho_\sigma. We bridge b_L to \ensuremath{\llbracket s \rrbracket((\rho_\sigma, b_t/x, c_t/y))} (the inner-LHS of the four-value pattern) via the four-value pattern of s \approx s (reflexive) at \Gamma', x:\ensuremath{\texttt{Nat}}, y:T[q(\sigma)], doubly-lifted substitution q^2(\sigma) \approx q^2(\sigma), and reflexive env-pair (\rho, b_t/x, c_t/y) \approx (\rho, b_t/x, c_t/y):

Hence by transitivity, b_L \approx \ensuremath{\llbracket s \rrbracket((\rho_\sigma, b_t/x, c_t/y))} \in R_O.

For b_I = \ensuremath{\llbracket s \rrbracket((\rho_\sigma, a/x, c/y))}: bridge to \ensuremath{\llbracket s \rrbracket((\rho_\sigma, b_t/x, c_t/y))} via ? on s at the env-pair related by:

giving \ensuremath{\llbracket s \rrbracket((\rho_\sigma, b_t/x, c_t/y))} \approx \ensuremath{\llbracket s \rrbracket((\rho_\sigma, a/x, c/y))} = b_I \in R_O. Hence b_L \approx b_I in R_O, and both are PER-related to the four-value pattern’s inner-LHS.

Symmetrically for the primed side. Combining: all four LHS values (\{b_L, b_I, b_I', b_L'\}) are pairwise related to the four RHS values (the four-value pattern of s outer/inner) in R_O, by transitivity through the inner-LHS/inner-RHS bridge.

Type part. The type four-value pattern is included in the application of \semtyeq[\Gamma, x:\ensuremath{\texttt{Nat}}, y:T]{s}{s}{T[\Uparrow \circ \Uparrow, \textsf{succ}~x_1/x]} above; by the same syntactic identity used for the term part, the goal’s type T[\textsf{succ}~t/x] pattern coincides with this type four-value pattern modulo the substitution-composition lemmas.

By ? on \ensuremath{\vDash \Gamma} we obtain \Gamma \approx \Gamma \searrow R_\Gamma. Let \Gamma' with \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. We verify the three clauses of \Gamma \vDash \ensuremath{\texttt{Ty}_{i}} \subseteq \ensuremath{\texttt{Ty}_{j}} at the level k := 1 + \max(i, j).

Since \ensuremath{\texttt{Ty}_{i}} and \ensuremath{\texttt{Ty}_{j}} are closed terms, for any substitution \tau and any environment \rho_0 we have \ensuremath{\texttt{Ty}_{i}}[\tau] = \ensuremath{\texttt{Ty}_{i}}, \ensuremath{\texttt{Ty}_{j}}[\tau] = \ensuremath{\texttt{Ty}_{j}}, and by evaluation of the universe constructor \ensuremath{\llbracket \ensuremath{\texttt{Ty}_{i}} \rrbracket(\rho_0)} = U_i, \ensuremath{\llbracket \ensuremath{\texttt{Ty}_{j}} \rrbracket(\rho_0)} = U_j.

Part (1).

Part (2). Symmetrically:

Part (3). By <:-Univ with i \le j and j < k:

Let \Gamma' with \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. Write \rho_\sigma := \ensuremath{\llbracket \sigma \rrbracket(\rho)} and \rho_{\sigma'} := \ensuremath{\llbracket \sigma' \rrbracket(\rho')}.

We must verify the three clauses of \Gamma \vDash \Pi(x:S_1).\,T_1 \subseteq \Pi(x:S_2).\,T_2. Computing the four type values via substitution and evaluation of \Pi:

Part (1). By ? applied to \semtyeq[\Gamma]{S_1}{S_1}{\ensuremath{\texttt{Ty}_{i}}} and \semtyeq[\Gamma, x:S_1]{T_1}{T_1}{\ensuremath{\texttt{Ty}_{i}}}, we obtain \semtyeq[\Gamma]{\Pi(x:S_1).\,T_1}{\Pi(x:S_1).\,T_1}{\ensuremath{\texttt{Ty}_{i}}}. Instantiating its type-side four-value relation at \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \ensuremath{\mathcal{D}}, the outer-LHS-vs-inner-LHS leg yields:

Part (2). Symmetrically, by ? on S_2 and T_2 and the outer-RHS-vs-inner-RHS leg of its type-side four-value relation at the same data:

Part (3). We must show \Pi(\ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)}, T_1, \rho_\sigma) \mathrel{<:_i} \Pi(\ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})}, T_2, \rho_{\sigma'}). We apply <:-Pi, which requires:

\ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)} \approx \ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})} \in \mathcal{U}_i \searrow R_I for some R_I; for every \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I, \ensuremath{\llbracket T_1 \rrbracket(\rho_\sigma, a/x)} \mathrel{<:_i} \ensuremath{\llbracket T_2 \rrbracket(\rho_{\sigma'}, a'/x)}; \Pi(\ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)}, T_1, \rho_\sigma) \approx \Pi(\ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)}, T_1, \rho_\sigma) \in \mathcal{U}_i and \Pi(\ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})}, T_2, \rho_{\sigma'}) \approx \Pi(\ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})}, T_2, \rho_{\sigma'}) \in \mathcal{U}_i.

(a) Domain. Instantiate the type-side four-value relation of \semtyeq[\Gamma]{S_1}{S_2}{\ensuremath{\texttt{Ty}_{i}}} at \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \ensuremath{\mathcal{D}}:

The inner-LHS-vs-inner-RHS pair gives \ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)} \approx \ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})} \in \mathcal{U}_i \searrow R_I.

(b) Codomain. By ? on \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \semtyeq[\Gamma]{S_1}{S_1}{\ensuremath{\texttt{Ty}_{i}}}:

By the first premise of the semantic substitution judgment, this carries (\Gamma', x:S_1[\sigma]) \approx (\Gamma', x:S_1[\sigma]) \searrow R'_{x:S_1[\sigma]} and (\Gamma, x:S_1) \approx (\Gamma, x:S_1) \searrow R_{\Gamma,x:S_1}.

Let \ensuremath{\mathcal{D}}_I :: a \approx a' \in R_I be given. By the biconditional of R'_{x:S_1[\sigma]} from Ctx-Ext, (\rho, a/x) \approx (\rho', a'/x) \in R'_{x:S_1[\sigma]} requires \rho \approx \rho' \in R' (which we have via \ensuremath{\mathcal{D}}) and a \approx a' \in R_H'(\ensuremath{\mathcal{D}}) where R_H' is the head family for R'_{x:S_1[\sigma]}, governed by \ensuremath{\llbracket S_1[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket S_1[\sigma] \rrbracket(\rho')} \in \mathcal{U}_i \searrow R_H'(\ensuremath{\mathcal{D}}). By ? on the same left type \ensuremath{\llbracket S_1[\sigma] \rrbracket(\rho)} that governs both R_I (from (a)) and R_H'(\ensuremath{\mathcal{D}}), R_I \Leftrightarrow R_H'(\ensuremath{\mathcal{D}}). Hence a \approx a' \in R_H'(\ensuremath{\mathcal{D}}), and (\rho, a/x) \approx (\rho', a'/x) \in R'_{x:S_1[\sigma]}.

Apply \Gamma, x:S_1 \vDash T_1 \subseteq T_2 at \Gamma', x:S_1[\sigma] (with R'_{x:S_1[\sigma]}), the lifted substitution \semtyeq[\Gamma', x:S_1[\sigma]]{q(\sigma)}{q(\sigma')}{\Gamma, x:S_1}, and (\rho, a/x) \approx (\rho', a'/x) \in R'_{x:S_1[\sigma]}:

We now bridge the inner-evaluations of q(\sigma) and q(\sigma') to the desired environments. Using the lifted-substitution four-value pattern (instantiated at the identity weakening on \Gamma', x:S_1[\sigma] with (\rho, a/x) \approx (\rho', a'/x)):

By ? on \semtyeq[\Gamma, x:S_1]{T_1}{T_1}{\ensuremath{\texttt{Ty}_{i}}} applied to the first relation, and on \semtyeq[\Gamma, x:S_2]{T_2}{T_2}{\ensuremath{\texttt{Ty}_{i}}} applied (after substituting S_1 for S_2 via the well-formedness premises) to the second:

By ? applied to the codomain subtyping above and these two \mathcal{U}_i-equivalences:

(c) Self-relatedness. By ? on \semtyeq[\Gamma]{S_1}{S_1}{\ensuremath{\texttt{Ty}_{i}}} and \semtyeq[\Gamma, x:S_1]{T_1}{T_1}{\ensuremath{\texttt{Ty}_{i}}} instantiated at the same data, the inner-LHS-vs-inner-LHS leg of the resulting type-side four-value relation gives \Pi(\ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)}, T_1, \rho_\sigma) \approx \Pi(\ensuremath{\llbracket S_1 \rrbracket(\rho_\sigma)}, T_1, \rho_\sigma) \in \mathcal{U}_i. Symmetrically for S_2, T_2: \Pi(\ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})}, T_2, \rho_{\sigma'}) \approx \Pi(\ensuremath{\llbracket S_2 \rrbracket(\rho_{\sigma'})}, T_2, \rho_{\sigma'}) \in \mathcal{U}_i.

Conclusion. By <:-Pi with the four ingredients (a)–(c):

Let \Gamma' with \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. Write \rho_\sigma := \ensuremath{\llbracket \sigma \rrbracket(\rho)} and \rho_{\sigma'} := \ensuremath{\llbracket \sigma' \rrbracket(\rho')}. We must establish each clause of \Gamma \vDash S \subseteq T.

Part (1). Instantiate the first hypothesis \Gamma \vDash S \subseteq T' at this data; its clause (1) gives the goal:

Part (2). Instantiate the second hypothesis \Gamma \vDash T' \subseteq T at the same data; its clause (2) gives the goal:

Part (3). From the two hypotheses at the same data:

All three clauses of \Gamma \vDash S \subseteq T are now established.

Let \Gamma' with \Gamma' \approx \Gamma' \searrow R', \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, and \ensuremath{\mathcal{D}} :: \rho \approx \rho' \in R' be given. Write \rho_\sigma := \ensuremath{\llbracket \sigma \rrbracket(\rho)} and \rho_{\sigma'} := \ensuremath{\llbracket \sigma' \rrbracket(\rho')}. We establish each clause of \Gamma \vDash S \subseteq T.

Part (1). Instantiate the type-side four-value relation of \semtyeq[\Gamma]{S}{T}{\ensuremath{\texttt{Ty}_{i}}} at \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma} and \ensuremath{\mathcal{D}}:

The outer-LHS-vs-inner-LHS leg gives \ensuremath{\llbracket S[\sigma] \rrbracket(\rho)} \approx \ensuremath{\llbracket S \rrbracket(\rho_\sigma)} \in \mathcal{U}_i, which is clause (1).

Part (2). Instantiate the type-side four-value relation of \semtyeq[\Gamma]{T}{T}{\ensuremath{\texttt{Ty}_{i}}} at the same data:

The outer-RHS-vs-inner-RHS leg gives \ensuremath{\llbracket T[\sigma'] \rrbracket(\rho')} \approx \ensuremath{\llbracket T \rrbracket(\rho_{\sigma'})} \in \mathcal{U}_i, which is clause (2).

Part (3). From the four-value relation in part (1), the inner-LHS-vs-inner-RHS leg gives:

By ?:

This is clause (3).

By mutual induction on the syntactic derivations. Each rule’s case follows by applying the corresponding semantic rule lemma (?, ?, ?, ?, ?, ?) to the IHs on the rule’s premises.

By the fundamental theorem (?, statement (3)): \semtyeq[\Gamma]{s}{t}{T}. Unfolding, this means: for all \Gamma' \approx \Gamma' \searrow R', all \semtyeq[\Gamma']{\sigma}{\sigma'}{\Gamma}, all \rho \approx \rho' \in R', the evaluations of s and t are related in the appropriate PER.

We instantiate at:

\Gamma' := \Gamma (by statement (1), \Gamma \approx \Gamma \searrow R for some R), \sigma := \sigma' := \ensuremath{\textsf{id}} (the identity substitution is semantic by ?), \rho := \rho' := {\uparrow}^\Gamma (the initial environment is in R by ?).

Let A = \ensuremath{\llbracket T \rrbracket({\uparrow}^\Gamma)}, a = \ensuremath{\llbracket s \rrbracket({\uparrow}^\Gamma)}, and b = \ensuremath{\llbracket t \rrbracket({\uparrow}^\Gamma)}. Then A \approx A \in \mathcal{U}_i \searrow R_T and a \approx b \in R_T.

By realizability (?): {\downarrow}^A(a) \approx {\downarrow}^A(b) \in \textsf{Nf}. Unfolding the definition of \textsf{Nf}: for all n, there exists w such that \textsf{R}^{\textsf{Nf}}_n({\downarrow}^A(a)) \searrow w and \textsf{R}^{\textsf{Nf}}_n({\downarrow}^A(b)) \searrow w.

Taking n = |\Gamma| (the length of \Gamma, which provides enough fresh names):

Hence \textsf{nbe}_\Gamma^T(s) = w = \textsf{nbe}_\Gamma^T(t).

By induction on \kweak[\Gamma]{\phi}{\Delta}.

By induction on \kweak[\Delta']{\phi}{\Gamma}.

By induction on the derivation of \Gamma \searrow \textsf{Sb}.

Case

\vdash \cdot holds by Ctx-Emp.

Case

By induction on the derivation a \in \mathcal{U}_i^\ast \searrow P \searrow \textbf{El}.

Case

Type predicate (1). Assume \typing[\Delta]{S}{\ensuremath{\texttt{Ty}_{i}}} \;\circledR\; \textsf{Neu}_i^e. By ?:

We must show \typing[\Delta']{S[\psi]}{\ensuremath{\texttt{Ty}_{i}}} \;\circledR\; \textsf{Neu}_i^e.

For the Kripke condition: take any \Delta'' with \kweak[\Delta'']{\phi'}{\Delta'}.

This establishes the Kripke condition for S[\psi] at \textsf{Neu}_i^e.

Term predicate (2). Assume \typing[\Delta]{t}{S} \;\circledR\; {\uparrow}^A(w) \in \textsf{Neu}_i^e. By ?:

By type-predicate monotonicity (just proved): \typing[\Delta']{S[\psi]}{\ensuremath{\texttt{Ty}_{i}}} \;\circledR\; \textsf{Neu}_i^e. \typing[\Delta']{t[\psi]}{S[\psi]} by ?. w \approx w \in \textsf{Ne} unchanged. Kripke condition: for \kweak[\Delta'']{\phi'}{\Delta'}, by ? \kweak[\Delta'']{\psi \circ \phi'}{\Delta}, hypothesis gives \textsf{R}^{\textsf{Ne}}_{|\Delta''|}(w) \searrow u and \tyequiv[\Delta'']{t[\psi \circ \phi']}{u}{S[\psi \circ \phi']}. By substitution composition: t[\psi \circ \phi'] = t[\psi][\phi'] and S[\psi \circ \phi'] = S[\psi][\phi'].

Case