# A Formalized Extension of the Substitution Lemma in Coq

Maria J. D. Lima Departamento de Ciência da Computação
Universidade de Brasília, Brasília, Brazil<EMAIL_ADDRESS>Departamento de
Ciência da Computação
Universidade de Brasília, Brasília, Brazil Flávio L. C. de Moura Departamento
de Ciência da Computação
Universidade de Brasília, Brasília, Brazil<EMAIL_ADDRESS>
###### Abstract

The substitution lemma is a renowned theorem within the realm of
$\lambda$-calculus theory and concerns the interactional behaviour of the
metasubstitution operation. In this work, we augment the $\lambda$-calculus’s
grammar with an uninterpreted explicit substitution operator, which allows the
use of our framework for different calculi with explicit substitutions. Our
primary contribution lies in verifying that, despite these modifications, the
substitution lemma continues to remain valid. This confirmation was achieved
using the Coq proof assistant. Our formalization methodology employs a nominal
approach, which provides a direct implementation of the $\alpha$-equivalence
concept. The strategy involved in variable renaming within the proofs presents
a challenge, specially on ensuring an exploration of the implications of our
extension to the grammar of the $\lambda$-calculus.

##  1 Introduction

In this work, we present a formalization of the substitution lemma [6] in a
general framework that extends the $\lambda$-calculus with an explicit
substitution operator using the Coq proof assistant [25]. The source code is
publicly available at

https://flaviomoura.info/files/msubst.v

The substitution lemma is an important result concerning the composition of
the substitution operation, and is usually presented as follows in the context
of the $\lambda$-calculus:

Let $t,u$ and $v$ be $\lambda$-terms, $x\neq y$ and $x\notin FV(v)$, where
$FV(v)$ is the set of free variables of $v$. Then
$\\{y:=v\\}\\{x:=u\\}t=\\{x:=\\{y:=v\\}u\\}\\{y:=v\\}t$.

This is a well known result already formalized in the context of the
$\lambda$-calculus [8]. Nevertheless, in the context of $\lambda$-calculi with
explicit substitutions its formalization is not trivial due to the interaction
between the metasubstitution and the explicit substitution operator. Our
formalization is done in a nominal setting that uses the
MetaLib111https://github.com/plclub/metalib package of Coq, but no particular
explicit substitution calculi is taken into account because the expected
behaviour between the metasubstitution operation with the explicit
substitutition constructor is the same regardless the calculus. The
formalization was done with Coq (platform) version 8.15.2, which already comes
with the Metalib package. The novel contributions of this work are twofold:

  1. 1.

The formalization is modular in the sense that no particular calculi with
explicit substitutions is taken into account. Therefore, we believe that this
formalization could be seen as a generic framework for proving properties of
these calculi that uses the substitution lemma in the nominal setting [17, 21,
22];

  2. 2.

A solution to a circularity problem in the proofs is given. It adds an axiom
to the formalization that allow a rewrite step inside a let expression. Such a
rewrite step is problematic and does not seem to have a trivial solution.

##  2 A syntactic extension of the $\lambda$-calculus

In this section, we present the framework of the formalization, which is based
on a nominal approach [13] where variables use names. In the nominal setting,
variables are represented by atoms that are structureless entities with a
decidable equality:

    Parameter eq_dec : forall x y : atom, {x = y} + {x <> y}.

therefore different names mean different atoms and different variables. The
nominal approach is close to the usual paper and pencil notation used in
$\lambda$-calculus, whose grammar of terms is given by:

$t::=x\mid\lambda_{x}.t\mid t\ t$ (1)

where $x$ represents a variable which is taken from an enumerable set,
$\lambda_{x}.t$ is an abstraction, and $t\ t$ is an application. The
abstraction is the only binding operator: in the expression $\lambda_{x}.t$,
$x$ binds in $t$, called the scope of the abstraction. This means that all
free occurrence of $x$ in $t$ is bound in $\lambda_{x}.t$. A variable that is
not in the scope of an abstraction is free. A variable in a term is either
bound or free, but note that a varible can occur both bound and free in a
term, as in $(\lambda_{y}.y)\ y$.

The main rule of the $\lambda$-calculus, named $\beta$-reduction, is given by:

$(\lambda_{x}.t)\ u\to_{\beta}\\{x:=u\\}t$ (2)

where $\\{x:=u\\}t$ represents the result of substituting all free occurrences
of variable $x$ in $t$ with $u$ in such a way that renaming of bound variable
may be done in order to avoid the variable capture of free variables. We call
$t$ the body of the metasubstitution, and $u$ its argument. In other words,
$\\{x:=u\\}t$ is a metanotation for a capture free substitution. For instance,
the $\lambda$-term $(\lambda_{x}\lambda_{y}.x\ y)\ y$ has both bound and free
occurrences of the variable $y$, and in order to $\beta$-reduce it, one has to
replace (or substitute) the free variable $y$ for all free occurrences of the
variable $x$ in the term $(\lambda_{y}.x\ y)$. But a straight substitution
will capture the free variable $y$, i.e. this means that the free occurrence
of $y$ before the $\beta$-reduction will become bound after the
$\beta$-reduction step. A renaming of bound variables may be done to avoid
such a capture, so in this example, one can take an $\alpha$-equivalent222A
formal definition of this notion will be given later in this section. term,
say $(\lambda_{z}.x\ z)$, and perform the $\beta$-step correctly as
$(\lambda_{x}\lambda_{y}.x\ y)\ y\to_{\beta}\lambda_{z}.y\ z$. Renaming of
variables in the nominal setting is done via a name-swapping, which is
formally defined as follows:

$(\\!\\!(x\ y)\\!\\!)z:=\left\\{\begin{array}[]{ll}y,&\mbox{ if }z=x;\\\
x,&\mbox{ if }z=y;\\\ z,&\mbox{ otherwise. }\\\ \end{array}\right.$

This notion can be extended to $\lambda$-terms in a straightfoward way:

$(x\ y)t:=\left\\{\begin{array}[]{ll}(\\!\\!(x\ y)\\!\\!)z,&\mbox{ if }t=z;\\\
\lambda_{(\\!\\!(x\ y)\\!\\!)z}.(x\ y)t_{1},&\mbox{ if
}t=\lambda_{z}.t_{1};\\\ (x\ y)t_{1}\ (x\ y)t_{2},&\mbox{ if }t=t_{1}\
t_{2}\\\ \end{array}\right.$ (3)

In the previous example, one could apply a swap to avoid the variable capture
in a way that, a swap is applied to the body of the abstraction before
applying the metasubstitution to it: $(\lambda_{x}\lambda_{y}.x\ y)\
y\to_{\beta}\\{x:=y\\}((y\ z)(\lambda_{y}.x\ y))=\\{x:=y\\}(\lambda_{z}.x\
z)=\lambda_{z}.y\ z$. Could we have used a variable substitution instead of a
swapping in the previous example? Absolutely. We could have done the reduction
as $(\lambda_{x}\lambda_{y}.x\ y)\
y\to_{\beta}\\{x:=y\\}(\\{y:=z\\}(\lambda_{y}.x\ y))=\\{x:=y\\}(\lambda_{z}.x\
z)=\lambda_{z}.y\ z$, but as we will shortly see, variable substitution is not
stable modulo $\alpha$-equivalence, while the swapping is, thereby rendering
it a more fitting choice when operating with $\alpha$-classes.

In what follows, we will adopt a mixed-notation approach, intertwining
metanotation with the equivalent Coq notation. This strategy aids in
elucidating the proof steps of the upcoming lemmas, enabling a clearer and
more detailed comprehension of each stage in the argumentation. The
corresponding Coq code for the swapping of variables, named vswap, is defined
as follows: Definition vswap (x:atom) (y:atom) (z:atom) := if (z == x) then y
else if (z == y) then x else z.

therefore, the swap $(\\!\\!(x\ y)\\!\\!)z$ is written in Coq as vswap x y z.
As a short example to acquaint ourselves with the Coq notation, let us show
how we will write the proofs: Lemma vswap  id: $\forall$ x y, vswap x x y = y.

Proof. The proof is by case analysis, and it is straightforward in both cases,
when x = y and x $\not=$ y. $\hfill\Box$

###  2.1 An explicit substitution operator

The extension of the swap operation to terms require an additional comment
because we will not work with the grammar (1), but rather, we will extend it
with an explicit substitution operator:

$t::=x\mid\lambda_{x}.t\mid t\ t\mid[x:=u]t$ (4)

where $[x:=u]t$ represents a term with an operator that will be evaluated with
specific rules of a substitution calculus. The intended meaning of the
explicit substitution is that it will simulate the metasubstitution. This
formalization aims to be a generic framework applicable to any calculi with
explicit substitutions using a named notation for variables. Therefore, we
will not specify rules about how one can simulate the metasubstitution, but it
is important to be aware that this is not a trivial task as one can easily
lose important properties of the original $\lambda$-calculus [19, 15].

Calculi with explicit substitutions are formalisms that deconstruct the
metasubstitution operation into finer-grained steps, thereby functioning as an
intermediary between the $\lambda$-calculus and its practical implementations.
In other words, these calculi shed light on the execution models of higher-
order languages. In fact, the development of a calculus with explicit
substitutions faithful to the $\lambda$-calculus, in the sense of the
preservation of some desired properties were the main motivation for such a
long list of calculi with explicit substitutions invented in the last decades
[2, 24, 7, 11, 20, 16, 9, 12, 18].

The following inductive definition corresponds to the grammar (4), where the
explicit substitution constructor, named n  sub, has a special notation.
Instead of writing n  sub t x u, we will write [x := u] t similarly to (4).
Accordingly, n  sexp denotes the set of nominal $\lambda$-expressions equipped
with an explicit substitution operator, which, for simplicity, we will refer
to as just “terms”. Inductive n  sexp : Set :=

$|$ n  var (x:atom)

$|$ n  abs (x:atom) (t:n  sexp)

$|$ n  app (t1:n  sexp) (t2:n  sexp)

$|$ n  sub (t1:n  sexp) (x:atom) (t2:n  sexp).

The size of a term, also written as $|t|$, and the set fv  nom of the free
variables of a term are defined as usual: Fixpoint size (t : n  sexp) : nat :=

match t with

$|$ n  var x $\Rightarrow$ 1

$|$ n  abs x t $\Rightarrow$ 1 + size t

$|$ n  app t1 t2 $\Rightarrow$ 1 + size t1 \+ size t2

$|$ n  sub t1 x t2 $\Rightarrow$ 1 + size t1 \+ size t2

end.

Fixpoint fv  nom (t : n  sexp) : atoms :=

match t with

$|$ n  var x $\Rightarrow$ {{x}}

$|$ n  abs x t1 $\Rightarrow$ remove x (fv  nom t1)

$|$ n  app t1 t2 $\Rightarrow$ fv  nom t1 ‘union‘ fv  nom t2

$|$ n  sub t1 x t2 $\Rightarrow$ (remove x (fv  nom t1)) ‘union‘ fv  nom t2

end.

The action of a permutation on a term, written $(x\ y)t$, is inductively
defined as in (3) with the additional case for the explicit substitution
operator:

$(x\ y)t:=\left\\{\begin{array}[]{ll}(\\!\\!(x\ y)\\!\\!)v,&\mbox{ if }t\mbox{
is the variable }v;\\\ \lambda_{(\\!\\!(x\ y)\\!\\!)z}.(x\ y)t_{1},&\mbox{ if
}t=\lambda_{z}.t_{1};\\\ (x\ y)t_{1}\ (x\ y)t_{2},&\mbox{ if }t=t_{1}\
t_{2};\\\ [(\\!\\!(x\ y)\\!\\!)z:=(x\ y)t_{2}](x\ y)t_{1},&\mbox{ if
}t=[z:=t_{2}]t_{1}.\end{array}\right.$

The corresponding Coq definition is given by the following recursive function:
Fixpoint swap (x:atom) (y:atom) (t:n  sexp) : n  sexp :=

match t with

$|$ n  var z $\Rightarrow$ n  var (vswap x y z)

$|$ n  abs z t1 $\Rightarrow$ n  abs (vswap x y z) (swap x y t1)

$|$ n  app t1 t2 $\Rightarrow$ n  app (swap x y t1) (swap x y t2)

$|$ n  sub t1 z t2 $\Rightarrow$ n  sub (swap x y t1) (vswap x y z) (swap x y
t2)

end.

The swap function has many interesting properties, but we will focus on the
ones that are more relevant to the proofs related to the substitution lemma.
Nevertheless, all lemmas can be found in the source code of the
formalization333https://flaviomoura.info/files/msubst.v. The next lemmas are
simple properties that are all proved by induction on the structure of term t:
Lemma swap  neq: $\forall$ x y z w, z $\not=$ w $\rightarrow$ vswap x y z
$\not=$ vswap x y w.

Lemma swap  size  eq : $\forall$ x y t, size (swap x y t) = size t.

Lemma swap  symmetric : $\forall$ t x y, swap x y t = swap y x t.

Lemma swap  involutive : $\forall$ t x y, swap x y (swap x y t) = t.

Lemma shuffle  swap : $\forall$ w y z t, w $\not=$ z $\rightarrow$ y $\not=$ z
$\rightarrow$ (swap w y (swap y z t)) = (swap w z (swap w y t)).

Lemma swap  equivariance : $\forall$ t x y z w, swap x y (swap z w t) = swap
(vswap x y z) (vswap x y w) (swap x y t).

Lemma fv  nom  swap : $\forall$ z y t, z ‘notin‘ fv  nom t $\rightarrow$ y
‘notin‘ fv  nom (swap y z t).

The standard proof strategy used so far is induction on the structure of
terms. Nevertheless, the builtin induction principle automatically generated
in Coq for the inductive definition n  sexp is not strong enough due to
swappings:

    forall P :n_sexp -> Prop,
     (forall x:atom, P(n_var x)) ->
     (forall (x:atom) (t:n_sexp), P t -> P(n_abs x t)) ->
     (forall t1:n_sexp, P t1 -> forall t2:n_sexp, P t2 -> P(n_app t1 t2)) ->
     (forall t1:n_sexp, P t1 -> forall (x:atom) (t2:n_sexp), P t2 -> P([x:=t2]t1)) ->
           forall t:n_sexp, P t

In fact, in general, the induction hypothesis in the abstraction case (resp.
explicit substitution case) refers to the body t of the abstraction (resp. t1
of the explicit substitution), while the goal involves a swap acting on the
body of the abstraction (resp. explicit substitution). In order to circunvet
this problem, we defined a customized induction principle based on the size of
terms: Lemma n  sexp  induction: $\forall$ P : n  sexp $\rightarrow$ Prop,
($\forall$ x, P (n  var x)) $\rightarrow$

($\forall$ t1 z, ($\forall$ t2 x y, size t2 = size t1 $\rightarrow$ P (swap x
y t2)) $\rightarrow$ P (n  abs z t1)) $\rightarrow$

($\forall$ t1 t2, P t1 $\rightarrow$ P t2 $\rightarrow$ P (n  app t1 t2))
$\rightarrow$

($\forall$ t1 t3 z, P t3 $\rightarrow$ ($\forall$ t2 x y, size t2 = size t1
$\rightarrow$ P (swap x y t2)) $\rightarrow$ P (n  sub t1 z t3)) $\rightarrow$
($\forall$ t, P t).

which states that in order to conclude that a certain property $P$ holds for
all terms, we need to prove that:

  1. 1.

$P$ must hold for any variable;

  2. 2.

If $P$ holds for the term $(x\ y)t_{2}$, where $t_{1}$ and $t_{2}$ have the
same size, then it also holds for the abstraction $\lambda_{z}.t_{1},\forall
x,y,z,t_{1}$ and $t_{2}$;

  3. 3.

If $P$ holds for the terms $t_{1}$ and $t_{2}$ the it also holds for the
application $t_{1}\ t_{2}$;

  4. 4.

If $P$ holds for the term $t_{3}$ and for the term $(x\ y)t_{2}$, where
$t_{1}$ and $t_{2}$ have the same size, then it also holds for the explicit
substitution $[z:=t_{3}]t_{1},\forall x,y,z,t_{1},t_{2}$ and $t_{3}$.

The following lemma is a first example of the use of the n  sexp  induction
principle: Lemma notin  fv  nom  equivariance: $\forall$ t x’ x y, x’ ‘notin‘
fv  nom t $\rightarrow$ vswap x y x’ ‘notin‘ fv  nom (swap x y t).

Proof. Note that in the paper and pencil notation, this lemma states that:

If $x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t)$ then $(\\!\\!(x\
y)\\!\\!)x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\ y)t)$.

The proof is by induction on the size of the term $t$.

  1. 1.

If $t$ is a variable, say $z$, then $x^{\prime}\neq z$ by hypothesis, and we
need to prove that $(\\!\\!(x\ y)\\!\\!)x^{\prime}\neq(\\!\\!(x\ y)\\!\\!)z$.
We conclude by lemma $swap\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptneq$.

  2. 2.

If is an abstraction, say $t=\lambda_{z}.t_{1}$, then we have by induction
hypothesis that if $x^{\prime}\notin(x\ y)t_{2}$ then $(\\!\\!(x_{0}\
y_{0})\\!\\!)x^{\prime}\notin(x_{0}\ y_{0})(x\ y)t_{2}$ for any term $t_{2}$
with the same size as $t_{1}$, and any variables $x,y,x_{0}$ and $y_{0}$. At
this point is important to notice that an structural induction would generate
an induction hypothesis with $t_{1}$ only, which is not strong enough to prove
the goal $(\\!\\!(x\ y)\\!\\!)x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\ y)\lambda_{z}.t_{1})$ that
has $(x\ y)t_{1}$ (and not $t_{1}$ alone!) after the propagation of the swap.
In addition, we have by hypothesis that $x^{\prime}\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(t_{1})\backslash\\{z\\}$. This means that either $x^{\prime}=z$
or $x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{1})$, and there are two
subcases:

    1. (a)

If $x^{\prime}=z$ then the goal is $(\\!\\!(x\ y)\\!\\!)z\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\
y)\lambda_{z}.t_{1})\Leftrightarrow$ $(\\!\\!(x\ y)\\!\\!)z\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{(\\!\\!(x\ y)\\!\\!)z}.(x\ y)t_{1})\Leftrightarrow$
$(\\!\\!(x\ y)\\!\\!)z\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\
y)t_{1})\backslash\\{(\\!\\!(x\ y)\\!\\!)z\\}$ we are done by lemma
$notin\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptremove\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002pt3$.444This is a lemma from Metalib library and it states that forall
(x y : atom) (s : atoms), x = y -> y ‘notin‘ remove x s.

    2. (b)

Otherwise, $x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{1})$, and we conclude using
the induction hypothesis taking $x_{0}=x$, $y_{0}=y$ and the universally
quantified variables $x$ and $y$ of the internal swap as the same variable (it
does not matter which one).

  3. 3.

The application case is straightforward from the induction hypothesis.

  4. 4.

The case of the explicit substitution, i.e. when $t=[z:=t_{2}]t_{1}$, we have
to prove that $(\\!\\!(x\ y)\\!\\!)x^{\prime}\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\
y)([z:=t_{2}]t_{1}))$. We then propagate the swap over the explicit
substitution operator and show, by the definition of $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom$, we
have to prove that both $(\\!\\!(x\ y)\\!\\!)x^{\prime}\notin(fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\
y)t_{1}))\backslash\\{(\\!\\!(x\ y)\\!\\!)z\\}$ and $(\\!\\!(x\
y)\\!\\!)x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\ y)t_{2})$.

    1. (a)

In the former case, the hypothesis $x^{\prime}\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(t_{1})\backslash\\{z\\}$ generates two subcases, either
$x^{\prime}=z$ or $x^{\prime}\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{1})$, and we conclude with
the same strategy of the abstraction case.

    2. (b)

The later case is straightforward by the induction hypothesis. $\hfill\Box$

The other direction is also true, but we skip the proof that is also by
induction on the size of term t: Lemma notin  fv  nom  remove  swap: $\forall$
t x’ x y, vswap x y x’ ‘notin‘ fv  nom (swap x y t) $\rightarrow$ x’ ‘notin‘
fv  nom t.

###  2.2 $\alpha$-equivalence

As usual in the standard presentations of the $\lambda$-calculus, we work with
terms modulo $\alpha$-equivalence. This means that $\lambda$-terms are
identified up to renaming of bound variables. For instance, all terms
$\lambda_{x}.x$, $\lambda_{y}.y$ and $\lambda_{z}.z$ are seen as the same term
which corresponds to the identity function. Formally, the notion of
$\alpha$-equivalence is defined by the following inference rules:

*[Right=(aeq  var)] x =_αx *[Right=(aeq  abs  same)]t_1 =_αt_2λ_x.t_1 =_αλ_x.t_2

*[Right=(aeq  abs  diff)]x ≠y x ∉fv(t_2) t_1 =_α(y x) t_2λ_x.t_1 =_αλ_y.t_2

*[Right=(aeq  app)]t_1 =_αt_1’ t_2 =_αt_2’t_1 t_2 =_αt_1’ t_2’ *[Right=(aeq  sub  same)]t_1 =_αt_1’ t_2 =_αt_2’[ x := t_2 ] t_1 =_α[ x := t_2’ ] t_1’

*[Right=(aeq  sub  diff)]t_2 =_αt_2’ x ≠y x ∉fv(t_1’) t_1 =_α(y x) t_1’[ x := t_2 ] t_1 =_α[ y := t_2’ ] t_1’

Each of these rules correspond to a constructor in the aeq inductive
definition below: Inductive aeq : n  sexp $\rightarrow$ n  sexp $\rightarrow$
Prop :=

$|$ aeq  var : $\forall$ x, aeq (n  var x) (n  var x)

$|$ aeq  abs  same : $\forall$ x t1 t2, aeq t1 t2 $\rightarrow$ aeq (n  abs x
t1)(n  abs x t2)

$|$ aeq  abs  diff : $\forall$ x y t1 t2, x $\not=$ y $\rightarrow$ x ‘notin‘
fv  nom t2 $\rightarrow$ aeq t1 (swap y x t2) $\rightarrow$

aeq (n  abs x t1) (n  abs y t2)

$|$ aeq  app : $\forall$ t1 t2 t1’ t2’, aeq t1 t1’ $\rightarrow$ aeq t2 t2’
$\rightarrow$ aeq (n  app t1 t2) (n  app t1’ t2’)

$|$ aeq  sub  same : $\forall$ t1 t2 t1’ t2’ x, aeq t1 t1’ $\rightarrow$ aeq
t2 t2’ $\rightarrow$ aeq ([x := t2] t1) ([x := t2’] t1’)

$|$ aeq  sub  diff : $\forall$ t1 t2 t1’ t2’ x y, aeq t2 t2’ $\rightarrow$ x
$\not=$ y $\rightarrow$ x ‘notin‘ fv  nom t1’ $\rightarrow$ aeq t1 (swap y x
t1’) $\rightarrow$

aeq ([x := t2] t1) ([y := t2’] t1’).

In what follows, we use a infix notation for $\alpha$-equivalence in the Coq
code. Therefore, we write t =a u instead of aeq t u. The above notion defines
an equivalence relation over the set n  sexp of nominal expressions with
explicit substitutions, i.e. the aeq relation is reflexive, symmetric and
transitive (proofs in the source
file555https://flaviomoura.info/files/msubst.v). In addition,
$\alpha$-equivalent terms have the same size, and the same set of free
variables: Lemma aeq  size: $\forall$ t1 t2, t1 =a t2 $\rightarrow$ size t1 =
size t2.

Lemma aeq  fv  nom : $\forall$ t1 t2, t1 =a t2 $\rightarrow$ fv  nom t1 [=] fv
nom t2.

The key point of the nominal approach is that the swap operation is stable
under $\alpha$-equivalence in the sense that, $t_{1}=_{\alpha}t_{2}$ if, and
only if $(x\ y)t_{1}=_{\alpha}(x\ y)t_{2},\forall t_{1},t_{2},x,y$. Note that
this is not true for renaming substitutions: in fact,
$\lambda_{x}.z=_{\alpha}\lambda_{y}.z$, but
$\\{z:=x\\}(\lambda_{x}.z)=\lambda_{x}.x\neq_{\alpha}\\{z:=x\\}\lambda_{y}.x(\lambda_{y}.z)$,
assuming that $x\neq y$. This stability result is formalized as follows:
Corollary aeq  swap: $\forall$ t1 t2 x y, t1 =a t2 $\leftrightarrow$ (swap x y
t1) =a (swap x y t2).

When both variables in a swap do not occur free in a term, it eventually
renames only bound variables, i.e. the action of this swap results in a term
that is $\alpha$-equivalent to the original term. This is the content of the
following lemma: Lemma swap  reduction: $\forall$ t x y, x ‘notin‘ fv  nom t
$\rightarrow$ y ‘notin‘ fv  nom t $\rightarrow$ (swap x y t) =a t.

There are several other interesting auxiliary properties that need to be
proved before achieving the substitution lemma. In what follows, we refer only
to the tricky or challenging ones, but the interested reader can have a
detailed look in the source file. Note that, swaps are introduced in proofs by
the rules aeq abs diff and aeq sub diff. As we will see, the proof steps
involving these rules are trick because a naïve strategy can easily get
blocked in a branch without proof. We conclude this section, with a lemma that
gives the conditions for two swaps with a common variable to be merged: Lemma
aeq  swap  swap: $\forall$ t x y z, z ‘notin‘ fv  nom t $\rightarrow$ x
‘notin‘ fv  nom t $\rightarrow$ (swap z x (swap x y t)) =a (swap z y t).

Proof. Before commenting this proof, we state the lemma with the pencil and
paper (meta)notation:

If $z\notin fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(t)$ and $x\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t)$ then $(z\ x)(x\
y)t=_{\alpha}(z\ y)t$.

Initially, observe the similarity of the left hand side (LHS) of the
$\alpha$-equation with the lemma shuffle  swap:

$\forall w\ y\ z\ t,w\neq z\to y\neq z\to(w\ y)((y\ z)t)=(w\ z)((w\ y)t)$

In order to use it, we need to have that both z $\not=$ y and x $\not=$ y. We
start comparing z and y:

  1. 1.

If $z=y$ then the right hand side (RHS) reduces to $t$ because the swap is
trivial, and the LHS also reduces to $t$ since swap is involutive.

  2. 2.

When $z\neq y$ then we proceed by comparing $x$ and $y$:

    1. (a)

If $x=y$ then both sides of the $\alpha$-equation reduces to $(z\ y)t$, and we
are done.

    2. (b)

Finally, when $x\neq y$, we can apply the lemma $shuffle\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptswap$, and
use lemma $aeq\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptswap$ to reduce the current goal to $(z\ x)t=_{\alpha}t$, and we
conclude by lemma $swap\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptreduction$ since both $z$ and $x$
are not in the set of free variables of the term $t$. $\hfill\Box$

##  3 The metasubstitution operation of the $\lambda$-calculus

As presented in Section 2, the main operation of the $\lambda$-calculus is the
$\beta$-reduction (2) that expresses how to evaluate a function applied to an
argument. The $\beta$-contractum $\\{x:=u\\}t$ represents a capture free in
the sense that no free variable becomes bound by the application of the
metasubstitution. This operation is in the meta level because it is outside
the grammar of the $\lambda$-calculus (and hence its name). In [6], Barendregt
defines it as follows:

$\\{x:=u\\}t=\left\\{\begin{array}[]{ll}u,&\mbox{ if }t=x;\\\ y,&\mbox{ if
}t=y\mbox{ and }x\neq y;\\\ \\{x:=u\\}t_{1}\ \\{x:=u\\}t_{2},&\mbox{ if
}t=t_{1}\ t_{2};\\\ \lambda_{y}.(\\{x:=u\\}t_{1}),&\mbox{ if
}t=\lambda_{y}.t_{1}.\end{array}\right.$

where it is assumed the so called “Barendregt’s variable convention”:

If $t_{1},t_{2},\ldots,t_{n}$ occur in a certain mathematical context (e.g.
definition, proof), then in these terms all bound variables are chosen to be
different from the free variables.

This means that we are assumming that both $x\neq y$ and $y\notin fv(u)$ in
the case $t=\lambda_{y}.t_{1}$. This approach is very convenient in informal
proofs because it avoids having to rename bound variables. In order to
formalize the capture free substitution, i.e. the metasubstitution, there are
different possible approaches. In our case, we perform a renaming of bound
variables whenever the metasubstitution is propagated inside a binder. In our
case, there are two binders: abstractions and explicit substitutions.

Let $t$ and $u$ be terms, and $x$ a variable. The result of substituting $u$
for the free ocurrences of $x$ in $t$, written $\\{x:=u\\}t$ is defined as
follows:

$\\{x:=u\\}t=\left\\{\begin{array}[]{l@{}l}u,&\mbox{ if }t=x;\\\ y,&\mbox{ if
}t=y\ (x\neq y);\\\ \\{x:=u\\}t_{1}\ \\{x:=u\\}t_{2},&\mbox{ if }t=t_{1}\
t_{2};\\\ \lambda_{x}.t_{1},&\mbox{ if }t=\lambda_{x}.t_{1};\\\
\lambda_{z}.(\\{x:=u\\}((y\ z)t_{1})),&\mbox{ if }t=\lambda_{y}.t_{1},x\neq
y,z\notin fv(t)\cup fv(u)\cup\\{x\\};\\\ [x:=\\{x:=u\\}t_{2}]t_{1},&\mbox{ if
}t=[x:=t_{2}]t_{1};\\\ [z:=\\{x:=u\\}t_{2}]\\{x:=u\\}((y\ z)t_{1}),&\mbox{ if
}t=[y:=t_{2}]t_{1},x\neq y,z\notin fv(t)\cup
fv(u)\cup\\{x\\}.\end{array}\right.$ (5)

and the corresponding Coq code is as follows: Function subst  rec  fun (t:n
sexp) (u :n  sexp) (x:atom) {measure size t} : n  sexp :=

match t with

$|$ n  var y $\Rightarrow$ if (x == y) then u else t

$|$ n  abs y t1 $\Rightarrow$ if (x == y) then t else let (z,  ) :=

atom  fresh (fv  nom u ‘union‘ fv  nom t ‘union‘ {{x}}) in n  abs z (subst
rec  fun (swap y z t1) u x)

$|$ n  app t1 t2 $\Rightarrow$ n  app (subst  rec  fun t1 u x) (subst  rec
fun t2 u x)

$|$ n  sub t1 y t2 $\Rightarrow$ if (x == y) then n  sub t1 y (subst  rec  fun
t2 u x) else let (z,  ) :=

atom  fresh (fv  nom u ‘union‘ fv  nom t ‘union‘ {{x}}) in

n  sub (subst  rec  fun (swap y z t1) u x) z (subst  rec  fun t2 u x) end.

Note that this function is not structurally recursive due to the swaps in the
recursive calls, and that’s why we need to provide the size of the term $t$ as
the measure parameter. Alternatively, a structurally recursive version of the
function subst  rec  fun can be found in the file nominal.v of the Metalib
library666https://github.com/plclub/metalib. It has the size of the term as an
explicit parameter in which the substitution will be performed, and hence one
has to deal with the size of the term in each recursive call. We write {x:=u}t
instead of subst  rec  fun t u x, and refer to it just as “metasubstitution”.
The following lemma states that if $x\notin fv(t)$ then
$\\{x:=u\\}t=_{\alpha}t$. In informal proofs the conclusion of this lemma is
usually stated as a syntactic equality, ı.e. $\\{x:=u\\}t=t$ instead of the
$\alpha$-equivalence, but the function subst  rec  fun renames bound variables
whenever the metasubstitution is propagated inside an abstraction or an
explicit substitution, even in the case that the metasubstitution has no
effect in the subterm it is propagated, as long as the variables of the
metasubstitution and the binder (abstraction or explicit substitution) are
different of each other. That’s why the syntactic equality does not hold here.
Lemma m  subst  notin: $\forall$ t u x, x ‘notin‘ fv  nom t $\rightarrow$ {x
:= u}t =a t.

Proof. The proof is done by induction on the size of the term t using n  sexp
induction defined above. The interesting cases are the abstraction and the
explicit substituion. We focus in the abstraction case, i.e. when
$t=\lambda_{y}.t_{1}$, where the goal to be proven is
$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\lambda_{y}.t_{1}$. We consider two
cases:

  1. 1.

If $x=y$ the result is trivial because both LHS and RHS are equal to
$\lambda_{y}.t_{1}$

  2. 2.

If $x\neq y$ , we have to prove that $\lambda_{z}.\\{x:=u\\}(y\
z)t_{1}=_{\alpha}\lambda_{y}.t_{1}$, where $z$ is a fresh name not in the set
$fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u)\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})\cup\\{x\\}$. The induction hypothesis express
the fact that every term with the same size as the body $t_{1}$ of the
abstraction satisfies the property to be proven: $\forall
t^{\prime},|t^{\prime}|=|t_{1}|\to\forall u\ x^{\prime}\ x_{0}\
y_{0},x^{\prime}\notin fv((x_{0}\
y_{0})t^{\prime})\to\\{x^{\prime}:=u\\}((x_{0}\ y_{0})t^{\prime})=_{\alpha}(x\
y)t^{\prime}$. Therefore, according to the definition of the metasubstitution
(function [subst_rec_fun]), the variable $y$ will be renamed to $z$, and the
metasubstitution is propagated inside the abstraction resulting in the
following goal: $\lambda_{z}.\\{x:=u\\}((z\
y)t_{1})=_{\alpha}\lambda_{y}.t_{1}$. Since $z\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})=fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{1})\backslash\\{y\\}$,
there are two cases to consider, either $z=y$ or $z\in fv(t_{1})$:

    1. (a)

$z=y$: In this case, we are done by the induction hypothesis taking
$x_{0}=y_{0}=y$, for instance.

    2. (b)

$z\neq y$: In this case, we can apply the rule aeq abs diff, resulting in the
goal $\\{x:=u\\}((y\ z)t_{1})=_{\alpha}(y\ z)t_{1}$ which holds by the
induction hypothesis, since $|(z\ y)t_{1}|=|t_{1}|$ and $x\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((y\
z)t_{1})$ because $x\neq z$, $x\neq y$ and $x\notin fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{1})$.

The explicit substitution case is also interesting, i.e. if
$t=[y:=t_{2}]t_{1}$, but it follows a similar strategy used in the abstraction
case for $t_{1}$. For $t_{2}$ the result follows from the induction
hypothesis. $\hfill\Box$ The following lemmas concern the expected behaviour
of the metasubstitution when the metasubstitution’s variable is equal to the
abstraction’s variable. Their proofs are straightforward from the definition
subst  rec  fun. The corresponding version when the metasubstitution’s
variable is different from the abstraction’s variable will be presented later.
Lemma m  subst  abs  eq: $\forall$ u x t, {x := u}(n  abs x t) = n  abs x t.

Lemma m  subst  sub  eq: $\forall$ u x t1 t2, {x := u}(n  sub t1 x t2) = n
sub t1 x ({x := u}t2).

We will now prove some stability results for the metasubstitution w.r.t.
$\alpha$-equivalence. More precisely, we will prove that if
$t=_{\alpha}t^{\prime}$ and $u=_{\alpha}u^{\prime}$ then
$\\{x:=u\\}t=_{\alpha}\\{x:=u^{\prime}\\}t^{\prime}$, where $x$ is a variable
and $t,t^{\prime},u$ and $u^{\prime}$ are terms. This proof is split in two
cases: firstly, we prove that if $u=_{\alpha}u^{\prime}$ then
$\\{x:=u\\}t=_{\alpha}\\{x:=u^{\prime}\\}t,\forall x,t,u,u^{\prime}$;
secondly, we prove that if $t=_{\alpha}t^{\prime}$ then
$\\{x:=u\\}t=_{\alpha}\\{x:=u\\}t^{\prime},\forall x,t,t^{\prime},u$. These
two cases are then combined through the transitivity of the
$\alpha$-equivalence relation. Nevertheless, this task was not straighforward.
Let’s follow the steps of our first trial. Lemma aeq  m  subst  in  trial:
$\forall$ t u u’ x, u =a u’ $\rightarrow$ ({x := u}t) =a ({x := u’}t).

Proof. The proof is done by induction on the size of term t, and we will focus
on the abstraction case, i.e. $t=\lambda_{y}.t_{1}$. The goal in this case is
$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\\{x:=u^{\prime}\\}(\lambda_{y}.t_{1})$.

  1. 1.

If $x=y$ then the result is trivial by lemma $m\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002pteq$.

  2. 2.

If $x\neq y$ then we need two fresh names in order to propagate the
metasubstitution inside the abstractions on each side of the
$\alpha$-equation. Let $x_{0}$ be a fresh name not in the set $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u)\cup
fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})\cup\\{x\\}$, and $x_{1}$ be a fresh name not
in the set $fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u^{\prime})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})\cup\\{x\\}$. After propagating the
metasubstitution we need to prove $\lambda_{x_{0}}.\\{x:=u\\}((y\
x_{0})t_{1})=_{\alpha}\lambda_{x_{1}}.\\{x:=u^{\prime}\\}((y\ x_{1})t_{1})$,
and we proceed by comparing $x_{0}$ and $x_{1}$:

    1. (a)

If $x_{0}=x_{1}$ then we are done by the induction hypothesis.

    2. (b)

Otherwise, we need to apply the rule $aeq\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptdiff$ and the goal is
$\\{x:=u\\}((y\ x_{0})t_{1})=_{\alpha}(x_{0}\ x_{1})(\\{x:=u^{\prime}\\}((y\
x_{1})t_{1}))$. But in order to proceed we need to know how to propagate the
swap inside the metasubstitution, which is the content of the following lemma:

Lemma swap  m  subst: $\forall$ t u x y z, swap y z ({x := u}t) =a ({(vswap y
z x) := (swap y z u)}(swap y z t)).

Proof. We write the statement of the lemma in metanotation before starting the
proof:

$\forall t\ u\ x\ y\ z,(y\ z)(\\{x:=u\\}t)=_{\alpha}\\{(\\!\\!(y\
z)\\!\\!)x:=(y\ z)u\\}(y\ z)t$

The proof is by induction on the size of the term t, and again we will focus
only on the abstraction case, i.e. when $t=\lambda_{w}.t_{1}$. The goal in
this case is $(y\ z)(\\{x:=u\\}(\lambda_{w}.t_{1}))=_{\alpha}\\{(\\!\\!(y\
z)\\!\\!)x:=(y\ z)u\\}((y\ z)\lambda_{w}.t_{1})$, and we proceed by comparing
$x$ and $w$.

  1. 1.

If $x=w$ the $\alpha$-equality is trivial.

  2. 2.

If $x\neq w$ then we need a fresh name, say $w_{0}$, to be able to propagate
the metasubstitution inside the abstraction on the LHS of the
$\alpha$-equation. The variable $w_{0}$ is taken such that it is not in the
set $fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u)\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{w}.t_{1})\cup\\{x\\}$, and we get the goal
$\lambda_{(\\!\\!(y\ z)\\!\\!)w_{0}}.(y\ z)(\\{x:=u\\}(w\
w_{0})t_{1})=_{\alpha}\\{(\\!\\!(y\ z)\\!\\!)x:=(y\ z)u\\}(\lambda_{(\\!\\!(y\
z)\\!\\!)w}.(y\ z)t_{1})$. Now we propagate the metasubstitution over the
abstraction in the RHS of the goal. Since $x\neq w$ implies $(\\!\\!(y\
z)\\!\\!)x\neq(\\!\\!(y\ z)\\!\\!)w$, we need another fresh name, say $w_{1}$,
not in the set $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((y\ z)u)\cup fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{(\\!\\!(y\ z)\\!\\!)w}.(y\ z)t_{1})\cup\\{(\\!\\!(y\
z)\\!\\!)x\\}$, and after the propagation we need to prove that
$\lambda_{(\\!\\!(y\ z)\\!\\!)w_{0}}.(y\ z)(\\{x:=u\\}(w\
w_{0})t_{1})=_{\alpha}\lambda_{w_{1}}.\\{(\\!\\!(y\ z)\\!\\!)x:=(y\
z)u\\}((w_{1}\ (\\!\\!(y\ z)\\!\\!)w)((y\ z)t_{1}))$. We consider two cases:
either $w_{1}=(\\!\\!(y\ z)\\!\\!)w_{0}$ or $w_{1}\neq(\\!\\!(y\
z)\\!\\!)w_{0}$. In the former case, we apply the rule aeq abs same and we are
done by the induction hypothesis. When $w_{1}\neq(\\!\\!(y\ z)\\!\\!)w_{0}$,
the application of the rule aeq abs diff generates the goal

$(w_{1}\ (\\!\\!(y\ z)\\!\\!)w_{0})(y\ z)(\\{x:=u\\}(w\
w_{0})t_{1})=_{\alpha}\\{(\\!\\!(y\ z)\\!\\!)x:=(y\ z)u\\}((w_{1}\ (\\!\\!(y\
z)\\!\\!)w)((y\ z)t_{1}))$ (6)

We can use the induction hypothesis to propagate the swap inside the
metasubstitution, and then we get an $\alpha$-equality with metasubstitution
as main operation on both sides, whose corresponding components are
$\alpha$-equivalent. In a more abstract way, we have to prove an
$\alpha$-equality of the form
$\\{x:=u\\}t=_{\alpha}\\{x:=u^{\prime}\\}t^{\prime}$, where
$t=_{\alpha}t^{\prime}$ and $u=_{\alpha}u^{\prime}$, but this is exactly what
we were trying to prove in the previous lemma.

Therefore, we are in a circular problem because both aeq  m  subst  in  trial
and swap  m  subst depend on each other to be proved!

Our solution to this problem consists in taking advantage of the fact that
$\alpha$-equivalent terms have the same set of free variables (see lemma aeq
fv  nom), and noting that the external swap in the LHS of (6) was generated by
the application of the rule aeq  abs  diff because the abstractions have
different bindings. Let’s go back to the proof of lemma aeq  m  subst  in:
Lemma aeq  m  subst  in: $\forall$ t u u’ x, u =a u’ $\rightarrow$ ({x := u}t)
=a ({x := u’}t).

Proof. We go directly to the abstraction case. When $t=\lambda_{y}.t_{1}$, the
goal is
$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\\{x:=u^{\prime}\\}(\lambda_{y}.t_{1})$.
If $x\neq y$ then the fresh name needed for the LHS must not belong to the set
$fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u)\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})\cup\\{x\\}$, while the fresh name for the RHS
must not belong to $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u^{\prime})\cup fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})\cup\\{x\\}$. These sets differ only by the
subsets $fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u)$ and $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u^{\prime})$. Nevertheless,
these subsets are equal because $u$ and $u^{\prime}$ are $\alpha$-equivalent
(see lemma aeq  fv  nom). Concretely, the current goal is as follows:

     (let (z, _) := atom_fresh (union (fv_nom u) (union (fv_nom (n_abs y t1))
             (singleton x))) in n_abs z (subst_rec_fun (swap y z t1) u x)) =a
     (let (z, _) := atom_fresh (union (fv_nom u’) (union (fv_nom (n_abs y t1))
                (singleton x))) in n_abs z (subst_rec_fun (swap y z t1) u’ x))

where the sets $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u)$ and $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u^{\prime})$ appear in different $let$ expressions, each one is
responsible for generating one fresh name. But since these sets are equal, if
one could replace $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u)$ by $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u^{\prime})$ (or vice-versa) then only one fresh name is
generated after evaluating the atom  fresh function. Nevertheless, the only
way that we managed to do such replacement was by adding the following axiom:

    Axiom Eq_implies_equality: forall t1 t2, t1 =a t2 -> fv_nom t1 = fv_nom t2.

This axiom is similar to lemma aeq  fv  nom where the set equality [=] was
replaced by the syntactic (Leibniz) equality =. Now, we can generate just one
fresh name and propagate the metasubstitution on both sides of the goal, and
we are done by the induction hypothesis. The case of the explicit substitution
is similar, and with this strategy we avoid both the rules aeq abs diff and
aeq sub diff that introduce swappings. $\hfill\Box$ The next lemma, named aeq
m  subst  out will benefit the strategy used in the previous proof, but it is
not straightfoward. Lemma aeq  m  subst  out: $\forall$ t t’ u x, t =a t’
$\rightarrow$ ({x := u}t) =a ({x := u}t’).

Proof. The proof is by induction on the size of the term t. Note that
induction on the hypothesis t =a t’ does not work due to a similar problem
involving swaps that appears when structural induction on t is used. The
abstraction and the explicit substitution are the interesting cases.

In the abstraction case, we need to prove that
$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\\{x:=u\\}t^{\prime}$, where
$\lambda_{y}.t_{1}=_{\alpha}t^{\prime}$ by hypothesis. Therefore, $t^{\prime}$
must be an abstraction, and according to our definition of
$\alpha$-equivalence there are two possible subcases:

  1. 1.

In the first subcase, $t^{\prime}=\lambda_{y}.t_{2}$, where
$t_{1}=_{\alpha}t_{2}$, and hence the current goal is
$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\\{x:=u\\}(\lambda_{y}.t_{2})$. We
proceed by comparing $x$ and $y$:

    1. (a)

If $x=y$ then, we are done by using twice lemma $m\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002pteq$.

    2. (b)

When $x\neq y$, then we need to propagate the metasubstitution on both sides
of the goal. On the LHS, we need a fresh name that is not in the set
$fv(u)\cup fv(\lambda_{y}.t_{1})\cup\\{x\\}$, while for the RHS, the fresh
name cannot belong to the set $fv(u)\cup fv(\lambda_{y}.t_{2})\cup\\{x\\}$.
From the hypothesis $t_{1}=_{\alpha}t_{2}$, we know, by lemma $aeq\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptfv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom$, that
the sets $fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(t_{1})$ and $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{2})$ are equal. Therefore,
we can take just one fresh name, say $z$, and propagate both metasubstitutions
over abstractions with the same binding, and we conclude with the induction
hypothesis.

  2. 2.

In the second subcase, $t^{\prime}=\lambda_{y_{0}}.t_{2}$, where
$t_{1}=_{\alpha}(y_{0}\ y)t_{2}$ and $y\neq y_{0}$. The current goal is

$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\\{x:=u\\}(\lambda_{y_{0}}.t_{2})$

and we proceed by comparing $x$ and $y$:

    1. (a)

If $x=y$ then the goal simplifies to
$\lambda_{y}.t_{1}=_{\alpha}\\{x:=u\\}(\lambda_{y_{0}}.t_{2})$ by lemma
$m\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptsubst\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptabs\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002pteq$, and we pick a fresh name $x$, that is not in the set $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u)\cup
fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y_{0}}.t_{2})\cup\\{y\\}$, and propagate the
metasubstitution on the RHS of the goal, resulting in the new goal
$\lambda_{y}.t_{1}=_{\alpha}\lambda_{x}.\\{y:=u\\}((y_{0}\ x)t_{2})$. Note
that the metasubstitution on the RHS has no effect in the term $(y_{0}\
x)t_{2}$ because $y\neq y_{0}$, $y\neq x$ and $y$ does not occur free in
$t_{2}$ and we conclude by hypothesis.

    2. (b)

If $x\neq y$ then we proceed by comparing $x$ and $y_{0}$ on the RHS, and the
proof, when $x=y_{0}$, is analogous to the previous subcase. When both $x\neq
y$ and $x\neq y_{0}$ then we need to propagate the metasubstitution on both
sides of the goal
$\\{x:=u\\}(\lambda_{y}.t_{1})=_{\alpha}\\{x:=u\\}(\lambda_{y_{0}}.t_{2})$. We
have that $\lambda_{y}.t_{1}=_{\alpha}\lambda_{y_{0}}.t_{2}$ and hence the
sets $fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}.t_{1})$ and $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(\lambda_{y_{0}}.t_{2})$ are
equal. Therefore, only one fresh name, say $x_{0}$, that is not in the set
$x_{0}\notin fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(u)\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y_{0}}.t_{2})\cup\\{x\\}$ is enough to fulfill the
conditions for propagating the metasubstitutions on both sides of the goal,
and we are done by the induction hypothesis.

  3. 3.

The explicit substitution operation is also interesting, but we will not
comment because we are running out of space. $\hfill\Box$

As a corollary, one can join the lemmas aeq  m  subst  in and aeq  m  subst
out as follows: Corollary aeq  m  subst  eq: $\forall$ t t’ u u’ x, t =a t’
$\rightarrow$ u =a u’ $\rightarrow$ ({x := u}t) =a ({x := u’}t’).

Now, we show how to propagate a swap inside metasubstitutions using the
decomposition of the metasubstitution provided by the corollary aeq  m  subst
eq.
Lemma swap  subst  rec  fun: $\forall$ x y z t u, swap x y ({z := u}t) =a
({(vswap x y z) := (swap x y u)}(swap x y t)).

Proof. Firstly, we write the lemma in metanotation: $\forall x\ y\ z\ t\ u,(x\
y)\\{z:=u\\}t=_{\alpha}\\{(\\!\\!(x\ y)\\!\\!)z:=(x\ y)u\\}(x\ y)t$. Next, we
compare $x$ and $y$, since the case $x=y$ is trivial. When $x\neq y$, the
proof proceeds by induction on the size of the term $t$. The tricky cases are
the abstraction and explicit substitution, and we comment just the former
case. If $t=\lambda_{y^{\prime}}.t_{1}$ then we must prove that $(x\
y)\\{z:=u\\}(\lambda_{y^{\prime}}.t_{1})=_{\alpha}\\{(\\!\\!(x\
y)\\!\\!)z:=(x\ y)u\\}(x\ y)(\lambda{y^{\prime}}.t_{1})$. Firstly, we compare
the variables $y^{\prime}$ and $z$ according to the definition of the
metasubstitution:

  1. 1.

When $y^{\prime}=z$ the metasubstitution is erased according to the definition
(5) on both sides of the goal and we are done.

  2. 2.

When $y^{\prime}\neq z$ then the metasubstitutions on both sides of the goal
need to be propagated inside the corresponding abstractions. In order to do
so, a new name need to be created. Note that in this case, it is not possible
to create a unique name for both sides because the two sets are different. In
fact, in the LHS the fresh name cannot belong to the set $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}^{\prime}.t_{1})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u)\cup\\{z\\}$, while the name
of the RHS cannot belong to the set $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\
y)\lambda_{y}^{\prime}.t_{1})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\ y)u)\cup\\{(\\!\\!(x\
y)\\!\\!)z\\}$. Let $x_{0}$ be a fresh name that is not in the set $fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{y}^{\prime}.t_{1})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(u)\cup\\{z\\}$, and $x_{1}$ a
fresh name that is not in the set $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\
y)\lambda_{y}^{\prime}.t_{1})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom((x\ y)u)\cup\\{(\\!\\!(x\
y)\\!\\!)z\\}$. After the propagation of the metasubstitutions, we have to
prove that $\lambda_{(\\!\\!(x\ y)\\!\\!)x0}.((x\ y)(\\{z:=u\\}((y^{\prime}\
x_{0})t_{1}))=_{\alpha}\lambda_{x_{1}}.(\\{(\\!\\!(x\ y)\\!\\!)z:=(x\
y)u\\}(((\\!\\!(x\ y)\\!\\!)y^{\prime})\ x_{1})((x\ y)t_{1}))$. We proceed by
comparing $x_{1}$ with $(\\!\\!(x\ y)\\!\\!)x_{0}$.

    1. (a)

If $x_{1}=(\\!\\!(x\ y)\\!\\!)x_{0}$ then we use the induction hypothesis to
propagate the swap inside the metasubstitution in the LHS, and we get the goal
$\\{(\\!\\!(x\ y)\\!\\!)z:=(x\ y)u\\}((x\ y)((y^{\prime}\
x_{0})t_{1}))=_{\alpha}\\{(\\!\\!(x\ y)\\!\\!)z:=(x\ y)u\\}((((\\!\\!(x\
y)\\!\\!)y^{\prime})\ ((\\!\\!(x\ y)\\!\\!)x_{0}))((x\ y)t_{1}))$ that is
proved by the swap equivariance lemma $swap\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptequivariance$.

    2. (b)

If $x_{1}\neq(\\!\\!(x\ y)\\!\\!)x_{0}$ then by the rule $aeq\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptdiff$ we
have to prove that the variable $(\\!\\!(x\ y)\\!\\!)x_{0}$ is not in the set
of free variables of the term $\\{(\\!\\!(x\ y)\\!\\!)z:=(x\
y)u\\}(((\\!\\!(x\ y)\\!\\!)y^{\prime}\ x_{1})(x\ y)t_{1})$ and that $(x\
y)(\\{z:=u\\}((y^{\prime}\ x_{0})t_{1}))=_{\alpha}(x_{1}\ ((\\!\\!(x\
y)\\!\\!)x_{0}))(\\{(\\!\\!(x\ y)\\!\\!)z:=(x\ y)u\\}((((\\!\\!(x\
y)\\!\\!)y^{\prime})\ x_{1})((x\ y)t_{1}))$. The former condition is routine.
The later condition is proved using the induction hypothesis twice to
propagate the swaps inside the metasubstitutions on each side of the
$\alpha$-equality. This swap has no effect on the variable $z$ of the
metasubstitution because $x_{1}$ is different from $(\\!\\!(x\ y)\\!\\!)z$,
and $x_{0}$ is different from $z$. Therefore we can apply lemma $aeq\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptm\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002pteq$, and
each generated case is proved by routine manipulation of swaps.

$\hfill\Box$

The following two lemmas toghether with lemmas m  subst  abs  eq and m  subst
sub  eq are essential in simplifying the propagations of metasubstitution.
They are presented here because they depend on lemma swap  subst  rec  fun.
Lemma m  subst  abs  neq: $\forall$ t u x y z, x $\not=$ y $\rightarrow$ z
‘notin‘ fv  nom u ‘union‘ fv  nom (n  abs y t) ‘union‘ {{x}} $\rightarrow$ {x
:= u}(n  abs y t) =a n  abs z ({x := u}(swap y z t)).

Lemma m  subst  sub  neq : $\forall$ t1 t2 u x y z, x $\not=$ y $\rightarrow$
z ‘notin‘ fv  nom u ‘union‘ fv  nom ([y := t2]t1) ‘union‘ {{x}} $\rightarrow$
{x := u}([y := t2]t1) =a ([z := ({x := u}t2)]({x := u}(swap y z t1))).

In the pure $\lambda$-calculus, the substitution lemma is probably the first
non trivial property. In our framework, we have defined two different
substitution operators, namely, the metasubstitution denoted by $\\{x:=u\\}t$
and the explicit substitution, written as $[x:=u]t$. In what follows, we
present the main steps of our proof of the substitution lemma for n  sexp
terms, i.e. for nominal terms with explicit substitutions. Lemma m  subst
lemma: $\forall$ t1 t2 t3 x y, x $\not=$ y $\rightarrow$ x ‘notin‘ (fv  nom
t3) $\rightarrow$

({y := t3}({x := t2}t1)) =a ({x := ({y := t3}t2)}({y := t3}t1)).

Proof. The proof is by induction on the size of t1. The interesting cases are
the abstraction and the explicit substitution. We focus on the former, i.e.
$t1=\lambda_{z}.t_{1}^{\prime}$, whose initial goal is

$\\{y:=t_{3}\\}(\\{x:=t_{2}\\}(\lambda_{z}.t_{1}^{\prime}))=_{\alpha}\\{x:=\\{y:=t_{3}\\}t_{2}\\}(\\{y:=t_{3}\\}(\lambda_{z}.t_{1}^{\prime}))$

assuming that $x\neq y$ and $x\notin fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{3})$. The induction
hypothesis generated by this case states that the lemma holds for any term of
the size of $t_{1}^{\prime}$, i.e. any term with the same size of the body of
the abstraction. We start comparing $z$ with $x$ aiming to apply the
definition of the metasubstitution on the LHS of the goal.

  1. 1.

When $z=x$, the subterm $\\{x:=t_{2}\\}\lambda_{x}.t_{1}^{\prime}$ reduces to
$\lambda_{x}.t_{1}^{\prime}$ by lemma $m\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002pteq$, and then the LHS reduces to
$\\{y:=t_{3}\\}\lambda_{x}.t_{1}^{\prime}$. The RHS
$\\{x:=\\{y:=t_{3}\\}t_{2}\\}\\{y:=t_{3}\\}\lambda_{x}.t_{1}^{\prime}$ also
reduces to it because $x$ does not occur free neither in
$\lambda_{x}.t_{1}^{\prime}$ nor in $t_{3}$, and we are done.

  2. 2.

When $z\neq x$, then we compare $y$ with $z$.

    1. (a)

When $y=z$, the subterm $\\{y:=t_{3}\\}(\lambda_{z}.t_{1}^{\prime})$ can be
simplified to $\lambda_{z}.t_{1}^{\prime}$, by lemma $m\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002pteq$. On the
LHS, we propagate the internal metasubstitution over the abstraction taking a
fresh name $w$ not in the set $fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{z}.t_{1}^{\prime})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{3})\cup fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(t_{2})\cup\\{x\\}$, where the goal is
$\\{z:=t_{3}\\}(\lambda_{w}.(\\{x:=t_{2}\\}(z\
w)t_{1}^{\prime}))=_{\alpha}\\{x:=\\{z:=t_{3}\\}t_{2}\\}(\lambda_{z}.t_{1}^{\prime})$.
We proceed by comparing $z$ and $w$:

      1. i.

If $z=w$ then the current goal simplifies to

$\\{w:=t_{3}\\}(\lambda_{w}.(\\{x:=t_{2}\\}t_{1}^{\prime}))=_{\alpha}\\{x:=\\{w:=t_{3}\\}t_{2}\\}(\lambda_{w}.t_{1}^{\prime})$

We can propagate the metasubstitution on the RHS and there is no need for a
fresh name since the variable $w$ fullfil the condition required by lemma
$m\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptsubst\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptabs\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptneq$. We conclude with lemmas $aeq\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptm\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptin$ and $m\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptnotin$.

      2. ii.

If $z\neq w$ then we can propagate the metasubstitutions on both sides of the
goal taking $w$ as the fresh name that fullfil the conditions of lemma $m\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptsubst\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptneq$. We
proceed with $aeq\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptabs\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptsame$, and conclude by the
induction hypothesis.

    2. (b)

If $y\neq z$ then we follow a similar strategy that avoids unnecessary
generation of fresh names. In this way, we take a fresh $w$ that is not in the
set $fv\kern 0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(t_{3})\cup fv\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptnom(t_{2})\cup fv\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern
0.80002ptnom(\lambda_{z}.t_{1}^{\prime})\cup\\{x\\}\cup\\{y\\}$, and propagate
the metasubstitution inside the abstraction resulting in the goal
$\lambda_{w}.(\\{y:=t_{3}\\}(\\{x:=t_{2}\\}(z\
w)t_{1}^{\prime})=_{\alpha}\lambda_{w}.(\\{x:=\\{y:=t_{3}\\}t_{2}\\}(\\{y:=t_{3}\\}(z\
w)t_{1}^{\prime})$. We conclude by the induction hypothesis. $\hfill\Box$

##  4 Conclusion and Future work

In this work, we presented a formalization of the substitution lemma in a
framework that extends the $\lambda$-calculus with an explicit substitution
operator. Calculi with explicit substitutions are important frameworks to
study properties of the $\lambda$-calculus and have been extensively studied
in the last decades [2, 3, 4, 5, 10].

The formalization is modular in the sense that the explicit substitution
operator is generic and could be instantiated with any calculi with explicit
substitutions in a nominal setting. Despite the fact that our definition of
metasubstitution, called $subst\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptrec\kern 0.80002pt\vbox{\hrule
width=3.50006pt,height=0.6pt}\kern 0.80002ptfun$, performs a renaming with a
fresh name whenever it is propagated inside a binding structure (either an
abstraction or an explicit substitution in our case), we showed how to avoid
unnecessary generation of fresh names that could result in a circular problem
in the proofs. Several auxiliary (minor) results were not included in this
document, but they are numerous and can be found in the source file of the
formalization that is publicly available at
https://flaviomoura.info/files/msubst.v

As future work, we intend to get rid of the axiom $Eq\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptimplies\kern
0.80002pt\vbox{\hrule width=3.50006pt,height=0.6pt}\kern 0.80002ptequality$.
The natural candidate for this would be the use of generalized rewriting, i.e.
setoid rewriting, but it not clear whether generalized rewriting allows a
rewrite step in a let expression. Another possibility is the implementation of
the metasubstitution using recursors [23, 14]. In addition, we plan to
integrate this formalization with another one related to the Z
property777https://cicm-conference.org/2021/cicm.php?event=fmm&menu=general to
prove confluence of calculi with explicit substitutions [21, 22], as well as
other properties in the nominal framework [17].

## References

  * [1]
  * [2] M. Abadi, L. Cardelli, P.-L. Curien & J.-J. Lévy (1991): _Explicit Substitutions_.  Journal of Functional Programming 1(4), pp. 375–416, 10.1017/S0956796800000186.
  * [3] Beniamino Accattoli (2012): _An Abstract Factorization Theorem for Explicit Substitutions_ , p. 16 pages.  10.4230/LIPICS.RTA.2012.6.
  * [4] Mauricio Ayala-Rincón, Flávio L.C. De Moura & Fairouz Kamareddine (2002): _Comparing Calculi of Explicit Substitutions with Eta-reduction_.  Electronic Notes in Theoretical Computer Science 67, pp. 76–95, 10.1016/S1571-0661(04)80542-5.
  * [5] Mauricio Ayala-Rincón, Flávio L.C. De Moura & Fairouz Kamareddine (2005): _Comparing and Implementing Calculi of Explicit Substitutions with Eta-Reduction_.  Annals of Pure and Applied Logic 134(1), pp. 5–41, 10.1016/j.apal.2004.06.009.
  * [6] H. P. Barendregt (1984): _The Lambda Calculus: Its Syntax and Semantics_ , rev. ed edition.  Studies in Logic and the Foundations of Mathematics v. 103, North-Holland ; Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co, Amsterdam ; New York : New York, N.Y.
  * [7] Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne & Jocelyne Rouyer-Degli (1996): _$\Lambda\nu$ , a Calculus of Explicit Substitutions Which Preserves Strong Normalisation_.  Journal of Functional Programming 6(5), pp. 699–722, 10.1017/S0956796800001945.
  * [8] Stefan Berghofer & Christian Urban (2007): _A Head-to-Head Comparison of de Bruijn Indices and Names_.  Electronic Notes in Theoretical Computer Science 174(5), pp. 53–67, 10.1016/j.entcs.2007.01.018.
  * [9] Roel Bloo & Herman Geuvers (1999): _Explicit Substitution: On the Edge of Strong Normalization_.  Theoretical Computer Science 211(1-2), pp. 375–395, 10.1016/s0304-3975(97)00183-7.
  * [10] E. Bonelli (2001): _Perpetuality in a Named Lambda Calculus With Explicit Substitutions_.  Mathematical Structures in Computer Science 11(1), pp. 47–90, 10.1017/s0960129500003248.
  * [11] Pierre-Louis Curien, Thérèse Hardin & Jean-Jacques Lévy (1996): _Confluence Properties of Weak and Strong Calculi of Explicit Substitutions_.  Journal of the ACM 43(2), pp. 362–397, 10.1145/226643.226675.
  * [12] R. David & B. Guillaume (2001): _A Lambda-Calculus with Explicit Weakening and Explicit Substitution_.  Mathematical Structures in Computer Science 11(1), pp. 169–206, 10.1017/S0960129500003224.
  * [13] Murdoch J. Gabbay & Andrew M. Pitts (2002): _A New Approach to Abstract Syntax with Variable Binding_.  Formal Aspects of Computing 13(3-5), pp. 341–363, 10.1007/s001650200016.
  * [14] Lorenzo Gheri & Andrei Popescu (2020): _A Formalized General Theory of Syntax with Bindings: Extended Version_.  Journal of Automated Reasoning 64(4), pp. 641–675, 10.1007/s10817-019-09522-2.
  * [15] Bruno Guillaume (2000): _The $\lambda$ _s_ _e_ -Calculus Does Not Preserve Strong Normalisation_.  Journal of Functional Programming 10(4), pp. 321–325, 10.1017/S0956796800003695.
  * [16] Fairouz Kamareddine & Alejandro Ríos (1997): _Extending a $\lambda$-Calculus with Explicit Substitution Which Preserves Strong Normalisation into a Confluent Calculus on Open Terms_.  Journal of Functional Programming 7(4), pp. 395–420, 10.1017/S0956796897002785.
  * [17] D. Kesner (2008): _Perpetuality for Full and Safe Composition (in a Constructive Setting)_.  In: Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II \- Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, pp. 311–322, 10.1007/978-3-540-70583-3_26.
  * [18] Delia Kesner (2009): _A Theory of Explicit Substitutions with Safe and Full Composition_.  Logical Methods in Computer Science Volume 5, Issue 3, p. 816, 10.2168/LMCS-5(3:1)2009.
  * [19] Paul-André Mellies (1995): _Typed $\lambda$-Calculi with Explicit Substitutions May Not Terminate_.  In Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Mariangiola Dezani-Ciancaglini & Gordon Plotkin, editors: Typed Lambda Calculi and Applications, 902, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 328–334, 10.1007/BFb0014062.
  * [20] C. A. Muñoz (1996): _Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus_.  In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pp. 440–447, 10.1109/LICS.1996.561460.
  * [21] Koji Nakazawa & Ken-etsu Fujita (2016): _Compositional Z: Confluence Proofs for Permutative Conversion_.  Studia Logica 104(6), pp. 1205–1224, 10.1007/s11225-016-9673-0.
  * [22] Koji Nakazawa, Ken-etsu Fujita & Yuta Imagawa (2023): _Z Property for the Shuffling Calculus_.  Mathematical Structures in Computer Science, pp. 1–13, 10.1017/S0960129522000408.
  * [23] Andrei Popescu (2023): _Nominal Recursors as Epi-Recursors_.  arXiv:https://arxiv.org/abs/2301.00894.
  * [24] K. H. Rose, R. Bloo & F. Lang (2011): _On Explicit Substitution With Names_.  J Autom Reasoning 49(2), pp. 275–300, 10.1007/s10817-011-9222-5.
  * [25] The Coq Development Team (2021): _The Coq Proof Assistant_.  Zenodo, 10.5281/ZENODO.5704840.