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);
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')];
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.
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 =
| Nil_ad : Ctx_adR [] []
| 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)];