1 Introduction↩︎

De Bruijn terms are a canonical technique for representing terms with binders [@de1972lambda], and have a long history of being used in mechanised formalisations of languages with binders in proof assistants. Despite this, they are often as regarded as cumbersome in practice [@aydemir2005mechanized], largely due to the overhead involved in proving and applying the many technical lemmas required for substitution and renaming.

The Autosubst code generator [@schafer2015autosubst; @stark2019autosubst] addresses this issue by automating reasoning about de Bruijn terms in the Rocq (formerly Coq) proof assistant in many cases. Given a signature describing a custom syntax, Autosubst automatically proves the substitution lemmas corresponding to the equations in the \(\sigma\)-calculus [@abadi1989explicit]. Central to the approach, Autosubst comes with a simplification tactic called asimpl which normalizes terms according to these equations. As the de Bruijn algebra forms a sound and complete model of the \(\sigma\)-calculus [@schafer2015], and as the rewriting system is convergent [@curien1996confluence], equality in the de Bruijn algebra is decidable by this tactic. In summary, this allows users to work with de Bruijn syntax without manually applying many technical lemmas.

However, this approach becomes less effective in situations where we want to unify a goal with an assumption, in Rocq’s case via the apply or eapply tactic. In particular, Autosubst’s automation is designed for assumption-free reasoning and does not support matching modulo \(\sigma\)-equivalence. As a consequence, the user must compensate for these limitations in their proof scripts. Common workarounds include stating rules in an indirect form to facilitate matching, introducing auxiliary lemmas with the right instantiations, and manually transforming goals during proofs to make them applicable, together with directly defining the values of appearing existential variables.

A representative example, is the formulation of the rule for type application in System \(F_{<:}\) in the POPLMark solution based on Autosubst:

[language=Coq, escapeinside={(*}{*)}]
    (*$T\_Tapp$*) : (*$\forall \;\Delta \;\Gamma \;s \;A \;A' \;B \;B'$*), (*$\Delta; \Gamma \vdash s: \forall A. B \to$*) (*$\Delta \vdash A' <: A \to$*) (*$B' = B[A' \cdot id]$*) 
                (* $ \to \Delta; \Gamma \vdash s \;A' : B'$*)

Here, the result type is expressed using a fresh meta-variable \(B'\) rather than the more direct expression \(B[A' \cdot id]\). While this formulation enables the use of the eapply tactic, it shifts the burden to the user, who (when applying this rule to a goal) must subsequently discharge the additional equality premise. This premise typically contains existential variables, and the asimpl tactic is only helpful in the case that the user can give the value of these existential variables upfront.

For example, proving the context morphism lemma in the POPLMark challenge, in the corresponding case we get stuck with the following goal

[language=Coq, escapeinside={(*}{*)}]
        (*$\Delta; \Gamma \vdash s[\sigma;\tau] \;A'[\sigma] : B[A'[\sigma] \cdot \sigma]$*)

where, when applying T_Tapp, we need to solve the equation \(B[A[\sigma] \cdot \sigma] = ?B[A[\sigma] \cdot id]\) with a constraint on \(?B\) as \(\Delta;\Gamma \vdash s[\sigma] : \forall A[\sigma]. ?B\).

Such indirect formulations are pervasive. They arise not only in typing rules, but also in reduction relations [@forster2019call; @abel2017poplmark], weakening and renaming lemmas, and even in mechanisations of dependent type theory [@adjedj2024martin]. Even when rules are stated directly, auxiliary lemmas are often introduced solely to make them compatible with apply.

This raises a natural question: can we recover the level of automation provided by Autosubst while supporting matching modulo \(\sigma\)-equivalence in the presence of assumptions?

The problem is inherently difficult. Moura et al. showed that Dowek et al.’s method [@dowek1995higher] does not decide second-order matching for the full \(\lambda\sigma\)-calculus [@de2005second], but even without \(\beta\), solutions are not necessarily unique. In practice, this means that a matching problem may admit multiple candidates, not all of which satisfy the premises in the context.

As a consequence, any practical solution must rely on heuristics. In the worst case, an adversarial example can always be constructed where a heuristic selects an incorrect solution, even when a correct one exists.

1.0.0.1 Contributions.

We extend the Autosubst framework with a tactic for pattern-matching modulo \(\sigma\)-equivalence. Our main contributions are as follows:

1. We introduce a heuristic tactic asapply, intended as a replacement for the apply/eapply tactic in Autosubst-based developments.

2. We generalize this tactic to support the full input language of Autosubst.

3. We evaluate our approach on several case studies, including the entire POPLMark and POPLMark Reloaded Challenge and show that despite its theoretical limitations, first results suggest it performs well in practice.

The development including all results is available online [@lfmtpRepo].

2 Background↩︎

We consider de Bruijn terms for the \(\lambda\)-calculus [@de1972lambda]: \[\begin{align} s,t \in \mathbb{T} \;::= \;n \;| \;s \;t \;| \;\lambda. s \qquad (n \in \mathbb{N}) \end{align}\] where \(s \;t\) denotes application, \(\lambda. s\) abstraction, and \(n\) are de Bruijn indices which serve as variables bound by abstraction. Parallel substitutions \(\sigma,\tau\) are total functions mapping indices to terms. Intuitively, a substitution can be seen as an infinite sequence of terms. Sometimes, we need to deal with a special kind of substitutions, written \(\xi,\zeta\), that map indices to indices known as renamings.

A de Bruijn algebra is a first-order two-sorted algebra formed of de Bruijn terms and substitutions, and certain constants and operations from the \(\sigma\)-calculus of Abadi et al. [@abadi1989explicit]. The central operation is instantiation: \(s[\sigma]\) replaces the free indices of the term \(s\) with the terms provided by the substitution \(\sigma\).

The \(\sigma\)-calculus comes with a defined set of primitives. The cons operation \(s \cdot \sigma\) prepends a term \(s\) to a substitution \(\sigma\). The composition of substitutions is defined as \((\sigma \circ \tau) \;n \;:= (\sigma \;n)[\tau]\). We further have constant substitutions such as the identity \(id \;:= \lambda n. n\) and the shift \(\uparrow \;:= \lambda n. (n+1)\). The lifting of a substitution is defined as and used as notation for \(\Uparrow \;\sigma := 0 \cdot \sigma \circ \uparrow\).

The \(\sigma\)-calculus is equipped with a directed set of equational rules over these primitives (Figure 1). We denote \(s\equiv_{\sigma'}t\) if \(s\) and \(t\) are provably equal by rewriting with a fragment \(\sigma'\) of \(\sigma\)-rules. We denote by \(\sigma_{\texttt{min}}\) the fragment consisting of the rules inside the box in Figure 1, which characterise instantiation and its compositionality properties.

Schäfer et al. showed that the de Bruijn algebra forms a sound and complete model of the \(\sigma\)-calculus [@schafer2015], and, as the rewriting system induced by these rules is known to be convergent [@curien1996confluence], equality in the de Bruijn algebra is decidable by normalisation with respect to the \(\sigma\)-rules.

We also require notions from \(\sigma\)-matching [@dowek1995higher; @baader1998term]. A \(\sigma\)-substitution \(\theta\) is a function from the object variables to \(\sigma\)-expressions such that \(\theta \;x \neq x\) for finitely many \(x\). Its domain is \(\mathcal{D}(\theta) := \{ x \;| \;\theta \;x \neq x\}\). We write \(\theta\) as \(\{x_1 \mapsto s_1,...,x_n \mapsto s_n\}\) where \(x_i \in \mathcal{D}(\theta)\) and denote its application to a \(\sigma\)-expression \(s\) simply as \({\theta} \ {s}\). Two substitutions \(\theta_1\) and \(\theta_2\) are \(\sigma'\)-equal iff \(\theta_1 \;x \equiv_{\sigma'} \theta_2 \;x\) for all \(x\). Otherwise, \(\theta_1\) and \(\theta_2\) are \(\sigma'\)-different.

We distinguish between bound and free object variables. The free variables \(\mathcal{F}(s)\) are the ones we need to resolve in a unification problem [@dowek1995higher]. We use the notation \(s=_{\sigma'} s'\) to denote a matching equation in a fragment \(\sigma'\) of the \(\sigma\)-calculus where \(s\) does not have free variables. We say \(s=_{\sigma'}t\) has a solution \(\theta\) iff \(s \equiv_{\sigma'} {\theta} \ {t}\) and \(\mathcal{D}(\theta) \subseteq \mathcal{F}(t)\). We call a \(\sigma'\)-matching algorithm \(\sigma\)-complete iff it computes all \(\sigma\)-different solutions to a \(\sigma'\)-matching problem. In our intended setting, bound variables correspond to abstract meta-variables, while free variables correspond to unresolved existential variables in a matching problem.

3 A Pattern Matching Tactic for Autosubst↩︎

We describe a general pattern-matching tactic asapply  for terms of the \(\lambda\)-calculus. The tactic is implemented in Rocq’s tactic language Ltac.

Let \(P\) be an \(n\)-ary relation, and consider the following Rocq goal:

[language=Coq, escapeinside={(*}{*)}]
(*$H \;: \;\forall $*) <qvars>, <premises> (*$ \to P \;t_1 \;t_2 \;... \;t_n $*) 
-------------------------------------------
(*$P \;s_1 \;s_2 \;... \;s_n$*)

with \(H\) an assumption in the context we want to apply, where <qvars> and <premises> denote the quantified variables and premises of \(H\).

A call of asapply  \(H\) proceeds in two phases: preprocessing and matching.

3.0.0.1 Preprocessing.

We first normalise both the goal and the conclusion of \(H\) with respect to the \(\sigma\)-calculus using the asimpl tactic provided by Autosubst.

Next, all quantified variables are replaced with existential variables (evars) of the corresponding types, which will be instantiated during matching. The premises of \(H\) are then turned into subgoals, to be solved after matching with instantiated quantified variables.

The actual matching will be between the corresponding \(s_i\) and \(t_i\). In a first step, we try whether this can be solved by pure syntactic matching using Rocq’s tactic. Furthermore, if \(s_i\) uses Autosubst’s explicit renamings (i.e., is of the form \(s\langle\xi\rangle\) or \(s[\xi]\)) but \(t_i\) is not, we change \(s_i\) to \(s[\xi]\) (\(s\langle\xi\rangle\)) using substify (renamify). These are Autosubst-provided tactics that perform conversion between instantiation and renaming operations.

3.0.0.2 Matching Phase.

After preprocessing, we obtain a \(\sigma\)-matching problem \[\mathcal{M}=\{s_i=_\sigma t_i \;| \;s_i \textrm{ and } t_i \textrm{ are } \sigma\textrm{-expressions} \}\] We process equations in \(\mathcal{M}\) from left to right.

For each equation \(s_i =_\sigma t_i\), we first try to match in the \(\sigma_{\texttt{min}}\) fragment using a procedure \(\sigma_{\texttt{min}}({s_i}, \ {t_i})\). If successful, this yields a substitution \(\theta\), which is applied to all remaining equations \(t_k\) for \(k \geq i\).

The function \(\sigma_{\texttt{min}}({s}, \ {t})\) is a partial procedure that computes substitutions by matching modulo the \(\sigma_{\texttt{min}}\) fragment. It proceeds as follows:

• If \(s\) and \(t\) match syntactically, a substitution is returned.

• Otherwise, \(t\) is rewritten using \(\sigma_{\texttt{min}}\) rules (Figure 1), and matching is retried.

In Figure 2, we give an operational description of the \(\sigma_{\texttt{min}}\)-function. The function performs a backtracking search over possible rewrites of \(t\) until a match with \(s\) is found. For example, \(\sigma_{\texttt{min}}(s[\sigma\circ \tau], \;?s[\tau])\) matches first with the seventh case, but the execution path stemming from it does not result in a \(\sigma\)-substitution. The execution backtracks and continues by matching with the tenth case, resulting in \(\{?s \mapsto s[\sigma]\}\).

If \(\sigma_{\texttt{min}}(s,t)\) fails, we apply a small set of heuristics capturing common patterns in developments:

• If \(s_i =_\sigma t_i\) is of the form \(s[t \cdot \sigma] =_\sigma ?s[t \cdot id]\), instantiate \(t_k\) with \(\{?s \mapsto s[\Uparrow \;\sigma]\}\), for \(k \geq i\).

• If \(s_i =_\sigma t_i\) is of the form \(s =_\sigma ?s[?\sigma]\), instantiate \(t_k\) with \(\{?s \mapsto s, \;\sigma \mapsto id\}\) respectively, for \(k \geq i\).

• If \(s_i =_\sigma t_i\) is of the form \(s =_\sigma ?s[id]\), instantiate \(t_k\) with \(\{?s \mapsto s\}\) respectively, for \(k \geq i\).

• If \(s_i =_\sigma t_i\) is of the form \(s =_\sigma s[?\sigma]\), instantiate \(t_k\) with \(\{?\sigma \mapsto id\}\) respectively, for \(k \geq i\).

We again \(\sigma\)-normalize \(H\) with the potentially instantiated existential variables. The tactic succeeds if the goal and \(H\) are syntactically equal at this point.

3.1 Generalisation↩︎

Autosubst [@stark2019autosubst] is a code generator that takes a second-order HOAS [@pfenning1988higher] representation of a custom syntax and generates a model of extended \(\sigma\)-calculus comprising multiple mutually inductive sorts, vector substitutions, and first-class renamings.

This tactic has been generalised to work for the input language of the Autosubst compiler. The \(\sigma_{\texttt{min}}\) fragment describes the instantiation operation and has compositionality laws. Hence, for a general syntax, the \(\sigma_{\texttt{min}}\)-function has congruence cases, and cases corresponding to the instantiation and compositionality laws.

If \(\sigma_{\texttt{min}}(s,t)\) fails, we check whether \(s=_\sigma t\) matches with certain equations that are recurring in developments. In the case of the first equation \(s[t \cdot \sigma]=_\sigma ?s[t \cdot id]\), the expression \(s[t \cdot id]\) denotes the elimination of the abstraction \(\lambda.s\) by substituting \(t\) for the bound index. We generate a case accordingly for each binder in the syntax. For example, if we have a polyadic binder \(\lambda_2 : (tm \to \;tm \to tm) \to tm\), we generate a case for the equation \(s[t_1 \cdot t_2 \cdot \sigma] = ?s[t_1 \cdot t_2 \cdot id]\). In the solution \(\{?s \mapsto s[\Uparrow \;\sigma]\}\) for the \(\lambda\)-abstraction, the substitution \(\Uparrow \sigma\) comes from the instantiation law \((\lambda.s)[\sigma]=\lambda.s[\Uparrow \;\sigma]\). For a general binder, this would be the lifted substitution vector formed during instantiation. In the case of \(\lambda_2\), the solution would be \(\{?s \mapsto s[\Uparrow\Uparrow \sigma]\}\) because \((\lambda_2.s)[\sigma] = \lambda_2.s[\Uparrow \Uparrow \;\sigma]\).

Note that as an additional difficulty since Autosubst supports first-class renamings, the \(\sigma_{\texttt{min}}\)-function and the specific equations have cases for the renaming operation, which we omit here for conciseness.

3.2 Current Limitations↩︎

We summarise some of the limitations of matching in the \(\sigma_{\texttt{min}}\) fragment and the asapplytactic.

First, note that, per se, the \(\sigma_{\texttt{min}}\) fragment is not a confluent rewrite system. The expression \((\lambda.s)[\sigma][\tau]\) reduces to both \(\lambda.s[0[\Uparrow \;\tau] \cdot \sigma \circ \uparrow \circ \Uparrow \tau ]\) and \(\lambda.s[0 \cdot \sigma \circ \tau \circ \uparrow]\) via \(\sigma_{\texttt{min}}\) rules. But, they are not joinable as \(\sigma_{\texttt{min}}\) lacks the rules \(0[s \cdot \sigma] \rightarrow s\) and \(\uparrow \circ (s \cdot \sigma) \rightarrow \sigma\). Of course they are joinable via the whole \(\sigma\)-calculus.

Note that \(\sigma_{\texttt{min}}\)-matching does not have unitary solutions in general. An example is \(s[\sigma \circ \tau]=_{\sigma_{\texttt{min}}}?s[?\sigma]\) which has two solutions \(\{?s \mapsto s, \;?\sigma \mapsto \sigma \circ \tau\}\) and \(\{?s \mapsto s[\sigma], \;?\sigma \mapsto \tau \}\).

Generally, asapplyis not \(\sigma\)-complete. In the above example, it would only produce the first solution. asapplyis not complete even as a decider. It fails for the equation \(t=_\sigma? s[t \cdot \sigma]\) though there is the solution \(\{?s \mapsto 0\}\). Note that this would rarely be a problem in a practical development.

4 Case Studies↩︎

We have tested the tactic on Rocq solutions of the POPLMark [@aydemir2005mechanized] and POPLMark Reloaded [@abel2017poplmark] challenges, two benchmarks on reasoning with binders. In this section, we present examples from our modified solutions. The linked development contains both the original and new solutions.

[language=Coq, escapeinside={(*}{*)}]
    (*$mstep\_inst$*) : (*$\forall \;s \;t \;\sigma$*), (*$s \ggcurly t \to$*) (*$s[\sigma] \ggcurly t[\sigma]$*)
    (*$H$*) : (*$\forall n$*), (*$\sigma \;n \ggcurly \tau \;n$*)
    --------------------------------------
    (*$(\sigma \;i)\langle\uparrow\rangle \ggcurly (\tau \;i)\langle\uparrow\rangle$*)

[language=Coq, escapeinside={(*}{*)}]
        (*$T\_Tapp$*) : (*$\forall \;\Delta \;\Gamma \;s \;A \;A' \;B$*), (*$\Delta; \Gamma \vdash s: \forall A. B \to$*) (*$\Delta \vdash A' <: A \to$*) (*$\Delta; \Gamma \vdash s \;A' : B[A' \cdot id]$*)
        (*$H_1$*) : (*$s[\sigma;\tau]$*) : (*$(\forall A . B)[\sigma]$*)
        (*$H_2$*) : (*$\Delta \vdash A'[\sigma] : A[\sigma]$*)
        --------------------------------------------------
        (*$\Delta; \Gamma \vdash s[\sigma;\tau] \;A'[\sigma] : B[A'[\sigma] \cdot \sigma]$*)

[language=Coq, escapeinside={(*}{*)}]
    (*$sub\_weak$*) : (*$\forall \Delta \;\Delta' \;\xi \;A_1 \;A_2$*), (*$\Delta \vdash A_1 <: A_2 \to$*) (*$(\forall x. (\Delta \;x)\langle\xi\rangle=\Delta'(\xi \;x))\to$*) (*$\Delta' \vdash A_1\langle \xi \rangle <: A_2\langle\xi\rangle$*)
    (*$H$*) : (*$\Delta \vdash B\langle\uparrow\rangle <: B'\langle\uparrow\rangle$*)
    ----------------------------------------------------
    (*$(B\langle\uparrow\rangle \cdot \Delta \circ \uparrow ) \vdash B\langle\uparrow\rangle <: B'\langle \xi \circ \uparrow\rangle$*) 

[language=Coq, escapeinside={(*}{*)}]
    (*$sub\_subst$*) : (*$\forall \Delta \;\Delta' \;\sigma \;A \;B$*), (*$\Delta \vdash A <: B \to$*) (*$(\forall x. \Delta' \vdash \sigma \;x <: (\Delta \;x)[\sigma])\to$*) (*$\Delta' \vdash A[\sigma] <: B[\sigma]$*)
    (*$H$*) : (*$\Delta \vdash A' <: A$*)
    ----------------------------------------------------
    (*$\Delta' \vdash A' <: A$*) 

4.0.0.1 Discussion.

Even in relatively short proof scripts such as the POPLMark challenge (642 lines) and POPLMark Reloaded (683 lines), the asapplyis used frequently: 15 times in the POPLMark B and 10 times in the POPLMark Reloaded. In all cases, it successfully solves the intended goal. Compared to the previous solutions, the proposed solutions with the matching tactics avoid the need for indirect definitions, auxiliary lemmas, and the need to manually transform the goal or find the instances for existential variables.

Additional (single) examples, for example, as one in a formalisation of Martin-Löf Type Theory [@adjedj2024martin], can be found in the appendix. These developments require a customised matching tactic due to manual adaptations of the substitution primitives in the original developments. Apart from these technical problems, both in this case study and in a development of the call-by-push-value [@forster2019call], we have so far not found any essential problems with the tactic.

5 Related Work↩︎

Mechanizing syntax has a long history, leading to many syntax representations [@de1972lambda; @aydemir2008engineering; @mcbride2004functional; @pfenning1988higher; @pitts2001nominal; @gordon1993mechanisation; @polesiuk2024functorial] and supporting tools [@schafer2015autosubst; @stark2019autosubst; @aydemir2010lngen; @keuchel2016needle; @sewell2010ott; @urban2012general; @van2025animating; @pientka2010beluga; @gacek2008abella; @schurmann2009twelf]. Autosubst [@schafer2015autosubst; @stark2019autosubst] provides automation for de Bruijn syntax and has been used in several mechanizations [@abel2017poplmark; @forster2019call; @adjedj2024martin; @forster2021completeness].

Unification in languages with binders has been studied extensively [@goubault2001higher]. Traditionally, unification is defined modulo \(\beta\eta\)-equivalence, known as higher-order unification. While higher-order unification is undecidable in general, Huet’s algorithm works well in practice [@huet1975unification]. Miller et al. [@miller1991logic] identify a fragment named higher-order patterns for which higher-order unification is decidable and is unitary, i.e. admits general unifiers. Higher-order matching is decidable up to fourth order [@padovani2000decidability] while for higher orders, decidability remains open.

Calculi for explicit substitutions such as the \(\sigma\)-calculus were introduced by Abadi et al. [@abadi1989explicit] to bridge the gap between the \(\lambda\)-calculus and its implementations. Curien et al. [@curien1996confluence] prove that the \(\sigma\)-calculus is a convergent rewriting system, and later Schäfer et al. [@schafer2015] show that the \(\sigma\)-calculus is a sound and complete model for the de Bruijn algebra. Together, this means the \(\sigma\)-calculus has practical usage as a rewriting system to decide equality in languages with binders as in the Autosubst library [@schafer2015autosubst; @stark2019autosubst]. However, these techniques do not directly extend to matching problems.

Dowek et al. [@dowek1995higher] show that higher-order unification is reducible to unification in the first-order equational theory of \(\lambda\sigma\)-calculus (\(\sigma\)-calculus with \(\beta\) rule), and provide a general unification method for the \(\lambda\sigma\)-calculus. Moura et al. [@de2005second] show that this method does not decide second-order matching in the \(\lambda\sigma\)-calculus by providing a non-terminating counter-example. They characterise a fragment for which the method terminates and provide a second-order matching algorithm for this fragment. This is not directly applicable as it covers the \(\sigma\)-calculus, including the \(\beta\) rule.

Nominal syntax [@gabbay2002new] provides an alternative representation of languages with binders. Urban et al. [@urban2004nominal] show that nominal unification is both decidable and unitary. Cheney [@cheney2005relating] shows that higher-order pattern unification problems can be solved by encoding them as nominal unification problems, and Levy et al. [@levy2008nominal] show the reverse. Nantes-Sobrinho et al. [@nantes2025nominal] generalise nominal unification problems to nominal equational problems and provide a rule-based algorithm to find solutions in the ground nominal algebra [@gabbay2002new].

Rocq’s original unification algorithm relies on heuristics [@ziliani2015unification]. Ziliani et al. [@ziliani2015unification] give a new unification algorithm along with an implementation for Calculus of Inductive Constructions, incorporating canonical structures and universe polymorphism. They formally describe a heuristic called controlled backtracking used in the unification algorithm of Rocq.

6 Conclusion and Ongoing Work↩︎

We extended the Autosubst framework to generate a pattern-matching tactic for custom syntax. The tactic is intended as a substitute for the apply tactic when matching with an assumption up to the substitution calculus. We tested this tactic on standard benchmarks, such as the POPLMark [@aydemir2005mechanized] and POPLMark Reloaded [@abel2017poplmark] challenges, and were able to simplify previous solutions.

The current tactic operates heuristically for pragmatic reasons – the \(\sigma\)-matching problem could potentially have many and even infinite solutions. However, in case the solution is not unique, it could produce an incorrect solution when there is a correct solution. Eventually, we are interested in having a matching tactic with proven guarantees; for example, we are interested in identifying the biggest fragment \(\sigma'\) for which the uniqueness criterion holds: If \(\theta\) is a solution of \(s=_{\sigma'}t\), then any other solution \(\theta'\) is \(\sigma\)-equal to \(\theta\).

7 More Examples↩︎

We look at more examples from the MLTT mechanization [@adjedj2024martin]¹, POPLMark Reloaded, and POPLMark to demonstrate the usefulness of our tactic.

[language=Coq,escapeinside={(*}{*)}]
(*$ty\_app$*) : (*$\forall$*) (*$\Gamma$*) ((*$f \;d \;dom \;cod:tm$*)), (*$\Gamma  \vdash f: \Pi_{dom} \;cod$*) -> (*$\Gamma \vdash d: dom $*) -> (*$\Gamma \vdash  tApp \;f \;d : cod[d \cdot id]$*)
(*$H$*) : (*$\Gamma \vdash a: dom\langle\xi\rangle$*)
-------------------------------------------
(*$\Gamma \vdash tApp \;n\langle\xi\rangle \;a \;: \;cod[a \cdot \xi]$*)

[language=Coq,escapeinside={(*}{*)}]
(*$ty\_wk$*) : (*$\forall$*) (*$\Gamma \;\Delta \;\xi$*), (*$\vdash \Delta$*) -> (*$\Gamma \vdash t : A$*) -> (*$\Delta \vdash t\langle \xi\rangle : A\langle\xi\rangle$*)
-------------------------------------------
(*$\Gamma \vdash n\langle\xi\rangle : \Pi_{dom\langle\xi\rangle} \;cod\langle\Uparrow \xi \rangle $*)

[language=Coq,escapeinside={(*}{*)}]
(*$\beta$*) : (*$\forall s \;t$*), (*$(\lambda.s) \;t \succ s[t \cdot id]$*) 
----------------------------
(*$\lambda. s[\Uparrow \sigma] \;t[\sigma] \succ s[t[\sigma] \cdot \sigma]$*)

[language=Coq,escapeinside={(*}{*)}]
(*$context\_renaming\_lemma$*) : (*$\forall \Delta' \;\Delta \;\Gamma \;\Gamma' \;s \;A \;\xi \;\zeta$*) ... -> (*$\Delta'; \Gamma' \vdash s: A$*) -> (*$\Delta; \Gamma \vdash s\langle\xi; \zeta\rangle : A\langle\xi\rangle$*) 
-------------------------------------------------
(*$\Delta' ; A[\sigma] \cdot \Gamma' \;\vdash \;(\tau \;f) \langle id; \uparrow\rangle : (\Gamma \;f)[\sigma]$*)