# Algorithmic Equality for the Untyped Lambda-calculus (R-version)

We discuss completeness of algorithmic equality for untyped lambda-terms with respect to declarative equality of lambda-terms. This case-study is part of ORBI, Open challenge problem Repository for systems reasoning with BInders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014).
The mechanization highlights several aspects:

• Induction on universally quantified objects
• First-class substitution variables
• Context weakening and strengthening with inductive inductives

### Syntax

Untyped lambda-terms are introduced with LF-level declarations. The context schemas translate directly from the ORBI file.

``````LF tm : type =
| app : tm → tm → tm
| lam : (tm → tm) → tm;
LF aeq : tm → tm → type =
| ae_l : ({x : tm} (aeq x x → aeq (M x) (N x))) → aeq (lam (λx. M x)) (lam (λx. N x))
| ae_a : aeq M1 N1 → aeq M2 N2 → aeq (app M1 M2) (app N1 N2);
schema xG = tm;
schema xaG = block (x:tm, u:aeq x x);
``````

## Context Relationships via Inductive Datatypes

The key to express context weakening and strengthening is the ability to relate two contexts via a substitution. In Beluga, we can describe context relations using inductive inductives as a relation between context `φ`, context `ψ`, and a substitution `σ` that maps variables from `φ` to the context `ψ`, formally `σ:[ψ ⊢ φ]` as follows:

``````inductive Ctx_xaR : {φ : xG} → {ψ : xaG} → [ψ ⊢ φ] → ctype =
| Nil_xa : Ctx_xaR [] [] [ ⊢ ^]
| Cons_xa : Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → Ctx_xaR [φ, x : tm] [ψ, b : block (x:tm, u:aeq x x)] [ψ, b ⊢ σ[…], b.1];
``````

The first-class substitution variable `σ` has domain `φ` and range `ψ`. If `σ` relates contexts `φ` and `ψ`, then the substitution `σ, b.1` relates `φ, x:tm` to `ψ, b:block (x:tm,u:aeq x x)` via constructor `Cons_xaR`.

``````inductive EqV : {φ : xG} → {ψ : xaG} → [ψ ⊢ φ] → {x : [φ ⊢ tm]} → {y : [ψ ⊢ tm]} → ctype =
| EqV_v : EqV [φ, x : tm] [ψ, b : block (x:tm, u:aeq x x)] [ψ, b : block (x:tm, u:aeq x x) ⊢ σ, b.1] [φ, x : tm ⊢ x] [ψ, b : block (x:tm, u:aeq x x) ⊢ b.1]
| EqV_p : EqV [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ #q.1] → EqV [φ, x : tm] [ψ, b : block (x:tm, u:aeq x x)] [ψ, b ⊢ σ[…], b.1] [φ, x : tm ⊢ #p[…]] [ψ, b : block (x:tm, u:aeq x x) ⊢ #q.1[…]];
inductive Eq : {φ : xG} → {ψ : xaG} → [ψ ⊢ φ] → {y1 : [φ ⊢ tm]} → {z : [ψ ⊢ tm]} → ctype =
| Eq_v : EqV [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ #q.1] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ #q.1]
| Eq_a : Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ M] [ψ ⊢ M'] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ N] [ψ ⊢ N'] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ app M N] [ψ ⊢ app M' N']
| Eq_l : Eq [φ, x : tm] [ψ, b : block (x:tm, u:aeq x x)] [ψ, b : block (x:tm, u:aeq x x) ⊢ σ[…], b.1] [φ, x : tm ⊢ M] [ψ, b : block (x:tm, u:aeq x x) ⊢ M'[…, b.1]] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ lam (λx. M)] [ψ ⊢ lam (λx. M')];
``````

### Proof of Reflexivity, Compact version

The recursive function `refl` of type `{φ:xG}{M: [φ ⊢ tm]} Ctx_xaR [φ] [ψ] [ ψ ⊢ σ ] → [ψ ⊢ aeq (M σ) (M σ)]`: for all contexts `φ` and `ψ` that have schema `xG` and `xaG`, respectively, if we have a substitution `σ` s.t. `σ:[ψ ⊢ φ]` then for all terms `M` depending on `φ`, we have a proof that `[ ψ ⊢ aeq (#p σ) (#p σ)]`." Since the term `M` depends only on the context `φ`, it is explicitly weakened through applying `σ` to move it to the context `ψ`.

``````rec ctx_membership : {#p : [φ ⊢ tm]} Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → [ψ ⊢ aeq (#p[σ]) (#p[σ])]  =
mlam p ⇒ fn cr ⇒ let  cr : Ctx_xaR [φ] [ψ] [ψ ⊢ σ]= cr in case [φ ⊢ #p] of
| [φ, x : tm ⊢ x] ⇒
let  Cons_xa cr' = cr in
let  cr' : Ctx_xaR [φ] [ψ] [ψ ⊢ σ]= cr' in [ψ, b : block (x:tm, u:aeq x x) ⊢ b.2]
| [φ, x : tm ⊢ #p[…]] ⇒
let  Cons_xa cr' = cr in
let  [ψ ⊢ E] = ctx_membership [φ ⊢ #p] cr' in [ψ, b : block (x:tm, u:aeq x x) ⊢ E[…]];
rec refl : {φ : xG} {M : [φ ⊢ tm]} Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → [ψ ⊢ aeq M[σ] M[σ]]  =
mlam φ ⇒ mlam M ⇒ fn cr ⇒ case [φ ⊢ M] of
| [φ ⊢ #p] ⇒ ctx_membership [φ ⊢ #p] cr
| [φ ⊢ app M N] ⇒
let  [ψ ⊢ D1] = refl [φ] [φ ⊢ M] cr in
let  [ψ ⊢ D2] = refl [φ] [φ ⊢ N] cr in [ψ ⊢ ae_a D1 D2]
| [φ ⊢ lam (λx. M)] ⇒
let  [ψ, b : block (x:tm, u:aeq x x) ⊢ D[…, b.1, b.2]] =
refl [φ, x : tm] [φ, x : tm ⊢ M] (Cons_xa cr) in [ψ ⊢ ae_l (λx. λu. D)];
``````

In the application case, we appeal to the induction hypothesis on `[φ ⊢ M]` and `[ ⊢ N]` through a recursive call. Since the context `φ` and the context `ψ` do not change, we can simply make the recursive all on `[φ ⊢ M]` and `[φ ⊢ M]` respectively using the relation `cr`.

When we have `[φ ⊢ lam λx.M ]`, we want to appeal to the induction hypothesis on `[φ, x:tm ⊢ M]`. In this instance, we also need a witness relating the context `[φ, x:tm ⊢ M]` to the context `[ψ, b:block (x:tm,u:aeq x x)]`. Recall that `cr` stands for `Ctx_xaR [φ] [ψ] [ψ ⊢ σ]`. Therefore, by `Cons_xa`, we know there exists `Ctx_xaR [φ ,x:tm] [ψ ,b:block (x:tm,u:aeq x x)] [ψ, b ⊢ σ, b.1]` and we appeal to the induction hypothesis by `reflR [φ,x:tm] [φ,x:tm.M] (Cons_xa cr)`.

Finally, we take a close look at the variable case. We distinguish two different cases depending on the position of the variable in the context by pattern matching on the shape of `φ`. If `[φ,x:tm ⊢ x]`, then we inspect the context relation `cr`. Pattern matching forces the original context `φ` to be `φ,x:tm`. By pattern matching on `cr'`, we observe that there exists a relation `cr'`, s.t. `Ctx_xaR [φ] [ψ] [ψ ⊢ σ]`. Moreover, `ψ = ψ,b:block (x:tm,u:aeq x x)` and `σ = σ, b.1` where the left hand side denotes the original context and substitution, while the right hand side shows the context and substitution refinement after pattern matching. We must show that there exists a proof for `aeq x x` in the context `ψ, b:block (x:tm,u:aeq x x)`. This is simply `b.2`.

Following we generalize reasoning about terms which contain substitution variables, reasoning explicitly about equality between terms `M` and `M[σ]`. Since we cannot pattern match directly on `M[σ]` (because `σ` is a general substitution and we do not enforce on the type-level that it is a variable-variable substitution) we cannot use unification to solve equations; If `σ` would be known to be a pattern substitution, then we could solve equations such as `M[σ] = app M1 M2`; we hence encode such equalities explicitly.

### Proof of Reflexivity, Expanded

``````rec ctx_member : {#p : [φ ⊢ tm]} Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → EqV [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ M] → [ψ ⊢ aeq M M]  =
mlam p ⇒ fn cr ⇒ fn m ⇒
let  cr : Ctx_xaR [φ] [ψ] [ψ ⊢ σ]= cr in case [φ ⊢ #p] of
| [φ, x : tm ⊢ x] ⇒
let  Cons_xa cr' = cr in
let  EqV_v = m in
let  cr' : Ctx_xaR [φ] [ψ] [ψ ⊢ σ]= cr' in [ψ, b : block (x:tm, u:aeq x x) ⊢ b.2]
| [φ, x : tm ⊢ #p[…]] ⇒
let  Cons_xa cr' = cr in
let  EqV_p m' = m in
let  [ψ ⊢ E] = ctx_member [φ ⊢ #p] cr' m' in [ψ, b : block (x:tm, u:aeq x x) ⊢ E[…]];
rec reflR : {φ : xG} {M : [φ ⊢ tm]} Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ M] [ψ ⊢ M'] → [ψ ⊢ aeq M' M']  =
mlam φ ⇒ mlam M ⇒ fn cr ⇒ fn m ⇒ case [φ ⊢ M] of
| [φ ⊢ #p] ⇒ let  Eq_v m' = m in ctx_member [φ ⊢ #p] cr m'
| [φ ⊢ app M N] ⇒
let  Eq_a m1 m2 = m in
let  [ψ ⊢ D1] = reflR [φ] [φ ⊢ M] cr m1 in
let  [ψ ⊢ D2] = reflR [φ] [φ ⊢ N] cr m2 in [ψ ⊢ ae_a D1 D2]
| [φ ⊢ lam (λx. M)] ⇒
let  Eq_l m' = m in
let  [ψ, b : block (x:tm, u:aeq x x) ⊢ D[…, b.1, b.2]] =
reflR [φ, x : tm] [φ, x : tm ⊢ M] (Cons_xa cr) m' in [ψ ⊢ ae_l (λx. λu. D)];
rec transV : Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → EqV [φ] [ψ] [ψ ⊢ σ] [φ ⊢ M] [ψ ⊢ #p.1] → EqV [φ] [ψ] [ψ ⊢ σ] [φ ⊢ N] [ψ ⊢ #p.1] → EqV [φ] [ψ] [ψ ⊢ σ] [φ ⊢ L] [ψ ⊢ #p.1] → [ψ ⊢ aeq #p.1 #p.1]  =
fn cr ⇒ fn m ⇒ fn n ⇒ fn l ⇒ case m of
| EqV_v  ⇒
let  EqV_v = n in
let  EqV_v = l in
let  Cons_xa cr' = cr in
let  cr' : Ctx_xaR [φ] [ψ] [ψ ⊢ σ]= cr' in [ψ, b : block (x:tm, u:aeq x x) ⊢ b.2]
| EqV_p m'  ⇒
let  EqV_p n' = n in
let  EqV_p l' = l in
let  Cons_xa cr' = cr in
let  [ψ ⊢ E] = transV cr' m' n' l' in [ψ, b : block (x:tm, u:aeq x x) ⊢ E[…]];
rec transR : Ctx_xaR [φ] [ψ] [ψ ⊢ σ] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ M] [ψ ⊢ M'] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ N] [ψ ⊢ N'] → Eq [φ] [ψ] [ψ ⊢ σ] [φ ⊢ L] [ψ ⊢ L'] → [ψ ⊢ aeq M' N'] → [ψ ⊢ aeq N' L'] → [ψ ⊢ aeq M' L']  =
fn cr ⇒ fn m ⇒ fn n ⇒ fn l ⇒ fn d1 ⇒ fn d2 ⇒ case d1 of
| [ψ ⊢ #p.2] ⇒
let  [ψ ⊢ #q.2] = d2 in
let  Eq_v m' = m in
let  m' : EqV [φ] [ψ, b : block (x:tm, u:aeq x x)] [ψ, b : block (x:tm, u:aeq x x) ⊢ σ] [φ ⊢ #r] [ψ, b : block (x:tm, u:aeq x x) ⊢ #q.1[…]]=
m' in ctx_member [φ ⊢ #r] cr m'
| [ψ ⊢ ae_a D1 D2] ⇒
let  [ψ ⊢ ae_a F1 F2] = d2 in
let  Eq_a m1 m2 = m in
let  Eq_a n1 n2 = n in
let  Eq_a l1 l2 = l in
let  [ψ ⊢ E1] = transR cr m1 n1 l1 [ψ ⊢ D1] [ψ ⊢ F1] in
let  [ψ ⊢ E2] = transR cr m2 n2 l2 [ψ ⊢ D2] [ψ ⊢ F2] in [ψ ⊢ ae_a E1 E2]
| [ψ ⊢ ae_l (λx. λu. D1)] ⇒
let  [ψ ⊢ ae_l (λx. λu. D2)] = d2 in
let  Eq_l m' = m in
let  Eq_l n' = n in
let  Eq_l l' = l in
let  [ψ, b : block (x:tm, u:aeq x x) ⊢ F[…, b.1, b.2]] =
transR (Cons_xa cr) m' n' l' [ψ, b : block (x:tm, u:aeq x x) ⊢ D1[…, b.1, b.2]] [ψ, b : block (x:tm, u:aeq x x) ⊢ D2[…, b.1, b.2]] in
[ψ ⊢ ae_l (λx. λu. F)];
deq : tm → tm → type.
de_l : ({x : tm} (deq x x → deq (M x) (M' x))) → deq (lam (λx. M x)) (lam (λx. M' x)).
de_a : deq M1 N1 → deq M2 N2 → deq (app M1 M2) (app N1 N2).
de_r : deq M M.
de_t : deq M L → deq L N → deq M N.
schema xdG = block (x:tm, de_v:deq x x);
schema daG = block (x:tm, ae_v:aeq x x, de_v:deq x x);
inductive Ctx_xdR : {φ : xG} → {ψ : xdG} → [ψ ⊢ φ] → ctype =
| Nil_xd : Ctx_xdR [] [] [ ⊢ ^]
| Cons_xd : Ctx_xdR [φ] [ψ] [ψ ⊢ σ] → Ctx_xdR [φ, x : tm] [ψ, b : block (x:tm, u:deq x x)] [ψ, b ⊢ σ[…], b.1];
inductive Ctx_adR : {φ : xaG} → {ψ : xdG} → ctype =
| Cons_ad : Ctx_adR [φ] [ψ] → Ctx_adR [φ, b : block (x:tm, u:aeq x x)] [ψ, b : block (x:tm, u:deq x x)];
``````

Equality in addition to properties about equality, such as deterministic and existence. These properties are all encoded relationally, because we do not support functions in computation-level types. If we were to support functions in computation-level types, these proofs and some of these relations would go away.

``````inductive EqV' : {φ : xG} → {ψ : xdG} → [ψ ⊢ φ] → {z1 : [φ ⊢ tm]} → {x1 : [ψ ⊢ tm]} → ctype =
| EqV'_v : EqV' [φ, x : tm] [ψ, b : block (x:tm, u:deq x x)] [ψ, b : block (x:tm, u:deq x x) ⊢ σ, b.1] [φ, x : tm ⊢ x] [ψ, b : block (x:tm, u:deq x x) ⊢ b.1]
| EqV'_p : EqV' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ #q.1] → EqV' [φ, x : tm] [ψ, b : block (x:tm, u:deq x x)] [ψ, b ⊢ σ[…], b.1] [φ, x : tm ⊢ #p[…]] [ψ, b : block (x:tm, u:deq x x) ⊢ #q.1[…]];
inductive Eq' : {φ : xG} → {ψ : xdG} → [ψ ⊢ φ] → {x2 : [φ ⊢ tm]} → {y2 : [ψ ⊢ tm]} → ctype =
| Eq'_v : EqV' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ #q.1] → Eq' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ #p] [ψ ⊢ #q.1]
| Eq'_a : Eq' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ M] [ψ ⊢ M'] → Eq' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ N] [ψ ⊢ N'] → Eq' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ app M N] [ψ ⊢ app M' N']
| Eq'_l : Eq' [φ, x : tm] [ψ, b : block (x:tm, u:deq x x)] [ψ, b : block (x:tm, u:deq x x) ⊢ σ[…], b.1] [φ, x : tm ⊢ M] [ψ, b : block (x:tm, u:deq x x) ⊢ M'[…, b.1]] → Eq' [φ] [ψ] [ψ ⊢ σ] [φ ⊢ lam (λx. M)] [ψ ⊢ lam (λx. M')];
inductive Equal_xaG : {ψ : xaG} → {y3 : [ψ ⊢ tm]} → {z2 : [ψ ⊢ tm]} → ctype =
| Refl_xaG : Equal_xaG [ψ ⊢ M] [ψ ⊢ M];
inductive Equal_xG : {ψ : xG} → {z3 : [ψ ⊢ tm]} → {x3 : [ψ ⊢ tm]} → ctype =
| Refl_xG : Equal_xG [ψ ⊢ M] [ψ ⊢ M];
inductive ExistsEq' : {γ : xG} → {φ : xdG} → [φ ⊢ γ] → {L : [φ ⊢ tm]} → ctype =
| ExistsEq' : {L : [γ ⊢ tm]} Eq' [γ] [φ] [φ ⊢ #T] [γ ⊢ L] [φ ⊢ Ld] → ExistsEq' [γ] [φ] [φ ⊢ #T] [φ ⊢ Ld]
| ExistsEqV' : {#p : [γ ⊢ tm]} EqV' [γ] [φ] [φ ⊢ #T] [γ ⊢ #p] [φ ⊢ #q.1] → ExistsEq' [γ] [φ] [φ ⊢ #T] [φ ⊢ #q.1];
rec existsEqV' : Ctx_xdR [γ] [φ] [φ ⊢ #T] → {#p : [φ ⊢ block (x:tm, u:deq x x)]} ExistsEq' [γ] [φ] [φ ⊢ #T] [φ ⊢ #p.1]  =
fn cr_xd ⇒ mlam p ⇒
let  cr_xd : Ctx_xdR [γ] [φ] [φ ⊢ #T]= cr_xd in case [φ ⊢ #p.1] of
| [φ, b : block (x:tm, u:deq x x) ⊢ b.1] ⇒
let  Cons_xd cr'_xd = cr_xd in
let  cr'_xd : Ctx_xdR [γ] [φ] [φ ⊢ #T]= cr'_xd in ExistsEqV' [γ, x : tm ⊢ x] EqV'_v
| [φ, b : block (x:tm, u:deq x x) ⊢ #p.1[…]] ⇒
let  Cons_xd cr'_xd = cr_xd in
let  ExistsEqV' ([γ ⊢ #r]) eq = existsEqV' cr'_xd [φ ⊢ #p] in ExistsEqV' [γ, x : tm ⊢ #r[…]] (EqV'_p eq);
rec existsEq' : Ctx_xdR [γ] [φ] [φ ⊢ #T] → {Ld : [φ ⊢ tm]} ExistsEq' [γ] [φ] [φ ⊢ #T] [φ ⊢ Ld]  =
fn cr_xd ⇒ mlam Ld ⇒
let  cr_xd : Ctx_xdR [γ] [φ] [φ ⊢ #T]= cr_xd in case [φ ⊢ Ld] of
| [φ ⊢ #p.1] ⇒ existsEqV' cr_xd [φ ⊢ #p]
| [φ ⊢ app M N] ⇒
let  ExistsEq' ([γ ⊢ L1]) eq1 = existsEq' cr_xd [φ ⊢ M] in
let  ExistsEq' ([γ ⊢ L2]) eq2 = existsEq' cr_xd [φ ⊢ N] in ExistsEq' [γ ⊢ app L1 L2] (Eq'_a eq1 eq2)
| [φ ⊢ lam (λx. M)] ⇒
let  ExistsEq' ([γ, x : tm ⊢ L]) eq =
existsEq' (Cons_xd cr_xd) [φ, b : block (x:tm, u:deq x x) ⊢ M[…, b.1]] in
ExistsEq' [γ ⊢ lam (λx. L)] (Eq'_l eq);
inductive ExistsEq : {γ : xG} → {ψ : xaG} → [ψ ⊢ γ] → {L : [γ ⊢ tm]} → ctype =
| ExistsEqV : {La : [ψ ⊢ tm]} EqV [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #p] [ψ ⊢ #q.1] → ExistsEq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #p]
| ExistsEq : {La : [ψ ⊢ tm]} Eq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ L] [ψ ⊢ La] → ExistsEq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ L];
rec existsEqV : Ctx_xaR [γ] [ψ] [ψ ⊢ σ] → {#p : [γ ⊢ tm]} ExistsEq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #p]  =
fn cr_xa ⇒ mlam p ⇒
let  cr_xa : Ctx_xaR [γ] [ψ] [ψ ⊢ σ]= cr_xa in case [γ ⊢ #p] of
| [γ, x : tm ⊢ x] ⇒
let  Cons_xa cr'_xa = cr_xa in
let  cr'_xa : Ctx_xaR [γ] [ψ] [ψ ⊢ σ]= cr'_xa in ExistsEqV [ψ, b : block (x:tm, u:aeq x x) ⊢ b.1] EqV_v
| [γ, x : tm ⊢ #p[…]] ⇒
let  Cons_xa cr'_xa = cr_xa in
let  ExistsEqV ([ψ ⊢ #q.1]) eq = existsEqV cr'_xa [γ ⊢ #p] in
let  eq : EqV [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #p] [ψ ⊢ #q.1]= eq in ExistsEqV [ψ, b : block (x:tm, u:aeq x x) ⊢ #q.1[…]] (EqV_p eq);
rec existsEq : Ctx_xaR [γ] [ψ] [ψ ⊢ σ] → {L : [γ ⊢ tm]} ExistsEq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ L]  =
fn cr_xa ⇒ mlam L ⇒
let  cr_xa : Ctx_xaR [γ] [ψ] [ψ ⊢ σ]= cr_xa in case [γ ⊢ L] of
| [γ ⊢ #p] ⇒ existsEqV cr_xa [γ ⊢ #p]
| [γ ⊢ app M N] ⇒
let  ExistsEq ([ψ ⊢ La1]) eq1 = existsEq cr_xa [γ ⊢ M] in
let  ExistsEq ([ψ ⊢ La2]) eq2 = existsEq cr_xa [γ ⊢ N] in ExistsEq [ψ ⊢ app La1 La2] (Eq_a eq1 eq2)
| [γ ⊢ lam (λx. M)] ⇒
let  ExistsEq ([ψ, b : block (x:tm, u:aeq x x) ⊢ La[…, b.1]]) eq =
existsEq (Cons_xa cr_xa) [γ, x : tm ⊢ M] in ExistsEq [ψ ⊢ lam (λx. La)] (Eq_l eq);
rec det_eqV : EqV [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #p] [ψ ⊢ #q.1] → EqV [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #p] [ψ ⊢ #r.1] → Equal_xaG [ψ ⊢ #q.1] [ψ ⊢ #r.1]  =
fn v ⇒ fn v' ⇒ case v of
| EqV_v  ⇒ let  EqV_v = v' in Refl_xaG
| EqV_p v  ⇒
let  EqV_p v' = v' in
let  Refl_xaG = det_eqV v v' in Refl_xaG;
rec det_eq : Eq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ M] [ψ ⊢ N] → Eq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ M] [ψ ⊢ N'] → Equal_xaG [ψ ⊢ N] [ψ ⊢ N']  =
fn m ⇒ fn m' ⇒ case m of
| Eq_v v  ⇒ let  Eq_v v' = m' in det_eqV v v'
| Eq_a m1 m2  ⇒
let  Eq_a n1 n2 = m' in
let  Refl_xaG = det_eq m1 n1 in
let  Refl_xaG = det_eq m2 n2 in Refl_xaG
| Eq_l m  ⇒
let  Eq_l n = m' in
let  Refl_xaG = det_eq m n in Refl_xaG;
rec det_eqV' : EqV' [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #q] [ψ ⊢ #p.1] → EqV' [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #r] [ψ ⊢ #p.1] → Equal_xG [γ ⊢ #q] [γ ⊢ #r]  =
fn v ⇒ fn v' ⇒ case v of
| EqV'_v  ⇒ let  EqV'_v = v' in Refl_xG
| EqV'_p v  ⇒
let  EqV'_p v' = v' in
let  Refl_xG = det_eqV' v v' in Refl_xG;
rec det_eq' : Eq' [γ] [ψ] [ψ ⊢ σ] [γ ⊢ M] [ψ ⊢ N] → Eq' [γ] [ψ] [ψ ⊢ σ] [γ ⊢ M'] [ψ ⊢ N] → Equal_xG [γ ⊢ M] [γ ⊢ M']  =
fn m ⇒ fn m' ⇒ case m of
| Eq'_v v  ⇒ let  Eq'_v v' = m' in det_eqV' v v'
| Eq'_a m1 m2  ⇒
let  Eq'_a n1 n2 = m' in
let  Refl_xG = det_eq' m1 n1 in
let  Refl_xG = det_eq' m2 n2 in Refl_xG
| Eq'_l m  ⇒
let  Eq'_l n = m' in
let  Refl_xG = det_eq' m n in Refl_xG;
rec ceq : Ctx_xaR [γ] [ψ] [ψ ⊢ σ] → Ctx_xdR [γ] [φ] [φ ⊢ #T] → Ctx_adR [ψ] [φ] → Eq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ M] [ψ ⊢ Ma] → Eq [γ] [ψ] [ψ ⊢ σ] [γ ⊢ N] [ψ ⊢ Na] → Eq' [γ] [φ] [φ ⊢ #T] [γ ⊢ M] [φ ⊢ Md] → Eq' [γ] [φ] [φ ⊢ #T] [γ ⊢ N] [φ ⊢ Nd] → [φ ⊢ deq Md Nd] → [ψ ⊢ aeq Ma Na]  =
fn cr_a ⇒ fn cr_d ⇒ fn cr_da ⇒ fn ma ⇒ fn na ⇒ fn md ⇒ fn nd ⇒ fn d ⇒
let  cr_da : Ctx_adR [ψ] [φ]= cr_da in
let  cr_a : Ctx_xaR [γ] [ψ] [ψ ⊢ σ]= cr_a in case d of
| [φ ⊢ #p.2] ⇒
let  Refl_xG = det_eq' md nd in
let  Refl_xaG = det_eq ma na in
let  Eq'_v v' = md in
let  Eq_v v = ma in
let  v : EqV [γ] [ψ] [ψ ⊢ σ] [γ ⊢ #r] [ψ ⊢ #q.1]= v in ctx_member [γ ⊢ #r] cr_a v
| [φ ⊢ de_r] ⇒
let  Refl_xG = det_eq' md nd in
let  Refl_xaG = det_eq ma na in reflR [γ] [γ ⊢ _] cr_a ma
| [φ ⊢ de_t D1 D2] ⇒
let  [φ ⊢ D1] : [φ ⊢ deq Md Ld]= [φ ⊢ D1] in
let  [φ ⊢ D2] : [φ ⊢ deq Ld Nd]= [φ ⊢ D2] in
let  ExistsEq' ([γ ⊢ L]) ld = existsEq' cr_d [φ ⊢ Ld] in
let  ExistsEq ([ψ ⊢ La]) la = existsEq cr_a [γ ⊢ L] in
let  [ψ ⊢ E1] = ceq cr_a cr_d cr_da ma la md ld [φ ⊢ D1] in
let  [ψ ⊢ E2] = ceq cr_a cr_d cr_da la na ld nd [φ ⊢ D2] in transR cr_a ma la na [ψ ⊢ E1] [ψ ⊢ E2]
| [φ ⊢ de_a D1 D2] ⇒
let  Eq_a ma1 ma2 = ma in
let  Eq'_a md1 md2 = md in
let  Eq_a na1 na2 = na in
let  Eq'_a nd1 nd2 = nd in
let  [ψ ⊢ E1] = ceq cr_a cr_d cr_da ma1 na1 md1 nd1 [φ ⊢ D1] in
let  [ψ ⊢ E2] = ceq cr_a cr_d cr_da ma2 na2 md2 nd2 [φ ⊢ D2] in [ψ ⊢ ae_a E1 E2]
| [φ ⊢ de_l (λx. λu. D)] ⇒
let  Eq_l ma1 = ma in
let  Eq'_l md1 = md in
let  Eq_l na1 = na in
let  Eq'_l nd1 = nd in
let  [ψ, b : block (x:tm, u:aeq x x) ⊢ E[…, b.1, b.2]] =
ceq (Cons_xa cr_a) (Cons_xd cr_d) (Cons_ad cr_da) ma1 na1 md1 nd1 [φ, b : block (x:tm, u:deq x x) ⊢ D[…, b.1, b.2]] in
[ψ ⊢ ae_l (λx. λu. E)];
``````