The mechanization highlights several aspects:

- Context exchange via substitution
- Free substitution property for parametric and hypothetical derivations
- Type reconstruction via inference

`tp : `type .

--name tp T.

arr : tp → tp → tp.

nat : tp.

tm : type .

--name tm M x.

app : tm → tm → tm.

lam : (tm → tm) → tm.

`pr`

of type `tm → tm → type`

defines parallel reduction, that M may reduce to M' or `M → M'`

. β-reduction `pr_b`

and its congruence rules `pr_l`

and `pr_a`

comprise the set of inference rules.
`pr : tm → tm → `type .

pr_l : ({x : tm} (pr x x → pr (M x) (N x))) → pr (lam M) (lam N).

pr_b : ({x : tm} (pr x x → pr (M x) (M' x))) → pr N N' → pr (app (lam M) N) (M' N').

pr_a : pr M M' → pr N N' → pr (app M N) (app M' N').

`oft`

which is indexed by terms `tm`

and types `tp`

. Constructors `of_app`

and `of_lam`

encode the typing rules for application and abstraction, respectively.
`oft : tm → tp → `type .

--name oft H.

of_app : oft M1 (arr T2 T) → oft M2 T2 → oft (app M1 M2) T.

of_lam : ({x : tm} (oft x T1 → oft (M x) T2)) → oft (lam M) (arr T1 T2).

schema rCtx = block (x:tm, pr_v:pr x x);

schema tCtx = some [t : tp] block (x:tm, of_v:oft x t);

schema trCtx = some [t : tp] block (x:tm, of_v:oft x t, pr_v:pr x x);

`S`

and `T`

cannot depend on the context `g`

, i.e. they are closed.rec subst : (g:tCtx) [g, b : block (x:tm, of_v:oft x T[]) ⊢ oft M[…, b.1] S[]] → [g ⊢ oft N T[]] → [g ⊢ oft M[…, N] S[]] =
fn d1 ⇒ fn d2 ⇒ let [g, b : block (x:tm, of_v:oft x T) ⊢ D1[…, b.1, b.2]] =
d1 in
let [g ⊢ D2] = d2 in [g ⊢ D1[…, _, D2]];

`M`

steps to `N`

and `M`

has type `A`

then `N`

has the same type `A`

. expressions to depend on the context since we may step terms containing variables. Substitution property for parametric and hypothetical derivations is free. We do not enforce here that the type `A`

is closed. Although this is possible by writing `A[]`

the statement looks simpler if we do not enforce this extra invariant.rec tps : (g:trCtx) [g ⊢ pr M N] → [g ⊢ oft M A] → [g ⊢ oft N A] =
fn r ⇒ fn d ⇒ case r of
| [g ⊢ #p.3] ⇒ d
| [g ⊢ pr_b (λx. λpr_v. R1) R2] ⇒
let [g ⊢ of_app (of_lam (λx. λof_v. D1)) D2] = d in
let [g, b : block (x:tm, of_v:oft x T, pr_v:pr x x) ⊢ F1[…, b.1, b.2]] =
tps [g, b : block (x:tm, of_v:oft x _, pr_v:pr x x) ⊢ R1[…, b.1, b.3]] [g, b ⊢ D1[…, b.1, b.2]] in
let [g ⊢ F2] = tps [g ⊢ R2] [g ⊢ D2] in [g ⊢ F1[…, _, F2]]
| [g ⊢ pr_l (λx. λpr_v. R)] ⇒
let [g ⊢ of_lam (λx. λof_v. D)] = d in
let [g, b : block (x:tm, of_v:oft x T, pr_v:pr x x) ⊢ F[…, b.1, b.2]] =
tps [g, b : block (x:tm, of_v:oft x _, pr_v:pr x x) ⊢ R[…, b.1, b.3]] [g, b ⊢ D[…, b.1, b.2]] in
[g ⊢ of_lam (λx. λof_v. F)]
| [g ⊢ pr_a R1 R2] ⇒
let [g ⊢ of_app D1 D2] = d in
let [g ⊢ F1] = tps [g ⊢ R1] [g ⊢ D1] in
let [g ⊢ F2] = tps [g ⊢ R2] [g ⊢ D2] in [g ⊢ of_app F1 F2];

The β-reduction case is perhaps the most note-worthy. We know by assumption that `d:[g ⊢ oft (app (lam A (λx. M x)) N)) (arr A B)`

and by inversion that `d:[g ⊢ of_a (of_l λx. λu. D1 x u)D2 ]`

where `D1`

stands for `oft (M x) B`

in the extended context `g, x:tm , u:oft x A`

. Furthermore, `D2`

describes a derivation `oft N A`

. A recursive call on `D2`

yields `F2:oft N' A`

. Likewise, y the i.h. on `D1`

, we obtain a derivation `F1:oft M' B`

in `g, b:block (x:tm , of_x:oft x A)`

. We now want to substitute for `x`

the term `N'`

, and for the derivation `oft x A`

the derivation `F2`

. This is achieved by applying to `F1`

the substitution `…, _ F2)`

. Since in the program above we do not have the name `N`

available, we write an underscore and let Beluga's type reconstruction algorithm infer the appropriate name.