Built with Alectryon, running Coq+SerAPI v8.17.0+0.17.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+πŸ–±οΈ to focus. On Mac, use ⌘ instead of Ctrl.

Un(i)typed Call-by-value Lambda Calculus

This file follows very closely its sibling CBVTyped.v. It is recommended to read that one first: the comments on this one will be quite more terse and focus on the differences.

Syntax

As our framework is "well-typed well-scoped", when we mean untyped, we really mean unityped, i.e., we will take the single element set as set of types. Although, the typing rules will not be as uninteresting as it would seem. Indeed, as we adopt a single-sided sequent-calculus style of presentation, we do give types to continuations (formally negated types), and we thus have not one type, but two: the type of terms βŠ• and the type of continuations βŠ–.

Typing contexts, terms, values, evaluation contexts and configurations work straightforwardly.

Variant ty : Type :=
| Left : ty
| Right : ty
.
Notation "βŠ•" := (Left) (at level 20) : ty_scope .
Notation "βŠ–" := (Right) (at level 20) : ty_scope .

Definition t_ctx : Type := Ctx.ctx ty .
Bind Scope ctx_scope with t_ctx .

Note that is is the proper pure untyped lambda calculus: in constrast with our STLC example, the lambda is not recursive and there is no unit value nor base type, only functions.

Inductive term (Ξ“ : t_ctx) : Type :=
| Val : val Ξ“ -> term Ξ“
| App : term Ξ“ -> term Ξ“ -> term Ξ“
with val (Ξ“ : t_ctx) : Type :=
| Var : Ξ“ βˆ‹ βŠ• -> val Ξ“
| Lam : term (Ξ“ β–Άβ‚“ βŠ•) -> val Ξ“
.
Inductive ev_ctx (Ξ“ : t_ctx) : Type :=
| K0 : Ξ“ βˆ‹ βŠ– -> ev_ctx Ξ“
| K1 : term Ξ“ -> ev_ctx Ξ“ -> ev_ctx Ξ“
| K2 : val Ξ“ -> ev_ctx Ξ“ -> ev_ctx Ξ“
.
Variant state (Ξ“ : t_ctx) : Type :=
| Cut : term Ξ“ -> ev_ctx Ξ“ -> state Ξ“
.

We introduce the sorted family of generalized values, together with the generalized variable.

Equations val_m : t_ctx -> ty -> Type :=
  val_m Ξ“ (βŠ•) := val Ξ“ ;
  val_m Ξ“ (βŠ–) := ev_ctx Ξ“ .

Equations a_id {Ξ“} : Ξ“ =[val_m]> Ξ“ :=
  a_id (βŠ•) i := Var i ;
  a_id (βŠ–) i := K0 i .

Substitution and Renaming

Equations t_rename {Ξ“ Ξ”} : Ξ“ βŠ† Ξ” -> term Ξ“ -> term Ξ” :=
  t_rename f (Val v)     := Val (v_rename f v) ;
  t_rename f (App t1 t2) := App (t_rename f t1) (t_rename f t2) ;
with v_rename {Ξ“ Ξ”} : Ξ“ βŠ† Ξ” -> val Ξ“ -> val Ξ” :=
  v_rename f (Var i) := Var (f _ i) ;
  v_rename f (Lam t) := Lam (t_rename (r_shift1 f) t) .

Equations e_rename {Ξ“ Ξ”} : Ξ“ βŠ† Ξ” -> ev_ctx Ξ“ -> ev_ctx Ξ” :=
  e_rename f (K0 i)   := K0 (f _ i) ;
  e_rename f (K1 t Ο€) := K1 (t_rename f t) (e_rename f Ο€) ;
  e_rename f (K2 v Ο€) := K2 (v_rename f v) (e_rename f Ο€) .

Equations s_rename {Ξ“ Ξ”} : Ξ“ βŠ† Ξ” -> state Ξ“ -> state Ξ” :=
  s_rename f (Cut t Ο€) := Cut (t_rename f t) (e_rename f Ο€).

Equations m_rename {Ξ“ Ξ”} : Ξ“ βŠ† Ξ” -> val_m Ξ“ β‡’α΅’ val_m Ξ” :=
  m_rename f (βŠ•) v := v_rename f v ;
  m_rename f (βŠ–) Ο€ := e_rename f Ο€ .

Renaming an assigment on the left.

Definition a_ren {Ξ“1 Ξ“2 Ξ“3} : Ξ“1 =[val_m]> Ξ“2 -> Ξ“2 βŠ† Ξ“3 -> Ξ“1 =[val_m]> Ξ“3 :=
  fun f g _ i => m_rename g _ (f _ i) .
Arguments a_ren _ _ _ /.

The following bunch of notations will help us to keep the code readable:

Notation "t β‚œβŠ›α΅£ r" := (t_rename r%asgn t) (at level 14).
Notation "v α΅₯βŠ›α΅£ r" := (v_rename r%asgn v) (at level 14).
Notation "Ο€ β‚‘βŠ›α΅£ r" := (e_rename r%asgn Ο€) (at level 14).
Notation "v β‚˜βŠ›α΅£ r" := (m_rename r%asgn _ v) (at level 14).
Notation "s β‚›βŠ›α΅£ r" := (s_rename r%asgn s) (at level 14).
Notation "a βŠ›α΅£ r" := (a_ren a%asgn r%asgn) (at level 14) : asgn_scope.

The weakenings we will need for substitution..

Definition t_shift1 {Ξ“ a} := @t_rename Ξ“ (Ξ“ β–Άβ‚“ a) r_pop.
Definition v_shift1 {Ξ“ a} := @v_rename Ξ“ (Ξ“ β–Άβ‚“ a) r_pop.
Definition m_shift1 {Ξ“ a} := @m_rename Ξ“ (Ξ“ β–Άβ‚“ a) r_pop.
Definition a_shift1 {Ξ“ Ξ” a} (f : Ξ“ =[val_m]> Ξ”) :=
  [ a_map f m_shift1 ,β‚“ a_id a top ]%asgn .

Substitutions

Equations t_subst {Ξ“ Ξ”} : Ξ“ =[val_m]> Ξ” -> term Ξ“ -> term Ξ” :=
  t_subst f (Val v)     := Val (v_subst f v) ;
  t_subst f (App t1 t2) := App (t_subst f t1) (t_subst f t2) ;
with v_subst {Ξ“ Ξ”} : Ξ“ =[val_m]> Ξ” -> val Ξ“ -> val Ξ” :=
  v_subst f (Var i) := f _ i ;
  v_subst f (Lam t) := Lam (t_subst (a_shift1 f) t) .

Equations e_subst {Ξ“ Ξ”} : Ξ“ =[val_m]> Ξ” -> ev_ctx Ξ“ -> ev_ctx Ξ” :=
  e_subst f (K0 i)   := f _ i ;
  e_subst f (K1 t Ο€) := K1 (t_subst f t) (e_subst f Ο€) ;
  e_subst f (K2 v Ο€) := K2 (v_subst f v) (e_subst f Ο€) .

Notation "t `β‚œβŠ› a" := (t_subst a%asgn t) (at level 30).
Notation "v `α΅₯βŠ› a" := (v_subst a%asgn v) (at level 30).
Notation "Ο€ `β‚‘βŠ› a" := (e_subst a%asgn Ο€) (at level 30).

Equations m_subst : val_m ⇒₁ ⟦ val_m , val_m βŸ§β‚ :=
  m_subst _ (βŠ•) v _ f := v `α΅₯βŠ› f ;
  m_subst _ (βŠ–) Ο€ _ f := Ο€ `β‚‘βŠ› f .

Equations s_subst : state β‡’β‚€ ⟦ val_m , state βŸ§β‚€ :=
  s_subst _ (Cut t Ο€) _ f := Cut (t `β‚œβŠ› f) (Ο€ `β‚‘βŠ› f) .

We can now instanciate the substitution monoid and module structures.

#[global] Instance val_m_monoid : subst_monoid val_m :=
  {| v_var := @a_id ; v_sub := m_subst |} .
#[global] Instance state_module : subst_module val_m state :=
  {| c_sub := s_subst |} .

Single-variable substitution.

Definition assign1 {Ξ“ a} v : (Ξ“ β–Άβ‚“ a) =[val_m]> Ξ“ := a_id ▢ₐ v .
Definition t_subst1 {Ξ“ a} (t : term _) v := t `β‚œβŠ› @assign1 Ξ“ a v.
Notation "t /[ v ]" := (t_subst1 t v) (at level 50, left associativity).

An Evaluator

Patterns and Observations

As before we define observations (copatterns), as there are only functions and continuations there is exactly one pattern at each type. Knowing this, we could have made this type (obs) disappear, but it is kept here for the sake of being more explicit.

Variant obs : ty -> Type :=
| ORet : obs (βŠ–)
| OApp : obs (βŠ•)
.

Observation still behave as binders, returning bind a term (what we are returning) and applying binds a term (the argument) and a continuation.

Equations obs_dom {a} : obs a -> t_ctx :=
  obs_dom (@ORet) := βˆ… β–Άβ‚“ βŠ• ;
  obs_dom (@OApp) := βˆ… β–Άβ‚“ βŠ• β–Άβ‚“ βŠ– .

Definition obs_op : Oper ty t_ctx :=
  {| o_op := obs ; o_dom := @obs_dom |} .
Notation ORet' := (ORet : o_op obs_op _).
Notation OApp' := (OApp : o_op obs_op _).

We now define applying an observation with arguments to a value.

Equations obs_app {Ξ“ a} (v : val_m Ξ“ a) (p : obs a) (Ξ³ : obs_dom p =[val_m]> Ξ“) : state Ξ“ :=
  obs_app v (OApp) Ξ³ := Cut (Val v) (K2 (Ξ³ _ (pop top)) (Ξ³ _ top)) ;
  obs_app Ο€ (ORet) Ξ³ := Cut (Val (Ξ³ _ top)) Ο€ .

Normal forms

Normal forms take the exact same form as for ULC: a head variable and an observation on it, with arguments.

Definition nf := c_var βˆ₯β‚› (obs_op # val_m).

The CBV Machine

The evaluator as a state machine.

  1. ⟨ t1 t2 | Ο€ ⟩ β†’ ⟨ t2 | t1 β‹…1 Ο€ ⟩
  2. ⟨ v | x ⟩ normal
  3. ⟨ v | t β‹…1 Ο€ ⟩ β†’ ⟨ t | v β‹…2 Ο€ ⟩
  4. ⟨ x | v β‹…2 Ο€ ⟩ normal
  5. ⟨ Ξ»x.t | v β‹…2 Ο€ ⟩ β†’ ⟨ t[x↦v] | Ο€ ⟩

Rules 1,3,5 step to a new configuration, while cases 2,4 are stuck on normal forms.

Equations eval_step {Ξ“ : t_ctx} : state Ξ“ -> (state Ξ“ + nf Ξ“) :=
  eval_step (Cut (App t1 t2)   (Ο€))      := inl (Cut t2 (K1 t1 Ο€)) ;
  eval_step (Cut (Val v)       (K0 i))   := inr (i β‹… ORet' ⦇ ! ▢ₐ v ⦈) ;
  eval_step (Cut (Val v)       (K1 t Ο€)) := inl (Cut t (K2 v Ο€)) ;
  eval_step (Cut (Val (Var i)) (K2 v Ο€)) := inr (i β‹… OApp' ⦇ ! ▢ₐ v ▢ₐ Ο€ ⦈) ;
  eval_step (Cut (Val (Lam t)) (K2 v Ο€)) := inl (Cut (t /[ v ]) Ο€) .

Definition ulc_eval {Ξ“ : t_ctx} : state Ξ“ -> delay (nf Ξ“)
  := iter_delay (ret_delay ∘ eval_step).

Properties

We now tackle the basic syntactic lemmas on renaming and substitution. See you in 400 lines.

Scheme term_mut := Induction for term Sort Prop
   with val_mut := Induction for val Sort Prop .

Record syn_ind_args (P_t : forall Ξ“, term Ξ“ -> Prop)
                    (P_v : forall Ξ“, val Ξ“ -> Prop)
                    (P_e : forall Ξ“, ev_ctx Ξ“ -> Prop) :=
  {
    ind_val {Ξ“} v (_ : P_v Ξ“ v) : P_t Ξ“ (Val v) ;
    ind_app {Ξ“} t1 (_ : P_t Ξ“ t1) t2 (_ : P_t Ξ“ t2) : P_t Ξ“ (App t1 t2) ;
    ind_var {Ξ“} i : P_v Ξ“ (Var i) ;
    ind_lam {Ξ“} t (_ : P_t _ t) : P_v Ξ“ (Lam t) ;
    ind_kvar {Ξ“} i : P_e Ξ“ (K0 i) ;
    ind_kfun {Ξ“} t (_ : P_t Ξ“ t) Ο€ (_ : P_e Ξ“ Ο€) : P_e Ξ“ (K1 t Ο€) ;
    ind_karg {Ξ“} v (_ : P_v Ξ“ v) Ο€ (_ : P_e Ξ“ Ο€) : P_e Ξ“ (K2 v Ο€)
  } .


P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
t: term Ξ“
P_t Ξ“ t

  destruct H; now apply (term_mut P_t P_v).
Qed.


P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
v: val Ξ“
P_v Ξ“ v

  destruct H; now apply (val_mut P_t P_v).
Qed.


P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
Ο€: ev_ctx Ξ“
P_e Ξ“ Ο€

  
P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
c: Ξ“ βˆ‹ βŠ–
P_e Ξ“ (K0 c)
P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
t: term Ξ“
Ο€: ev_ctx Ξ“
IHΟ€: P_e Ξ“ Ο€
P_e Ξ“ (K1 t Ο€)
P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
v: val Ξ“
Ο€: ev_ctx Ξ“
IHΟ€: P_e Ξ“ Ο€
P_e Ξ“ (K2 v Ο€)

  
P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
c: Ξ“ βˆ‹ βŠ–
P_e Ξ“ (K0 c)
 apply (ind_kvar _ _ _ H).
  
P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
t: term Ξ“
Ο€: ev_ctx Ξ“
IHΟ€: P_e Ξ“ Ο€
P_e Ξ“ (K1 t Ο€)
 apply (ind_kfun _ _ _ H); auto; apply (term_ind_mut _ _ _ H).
  
P_t: forall Ξ“ : t_ctx, term Ξ“ -> Prop
P_v: forall Ξ“ : t_ctx, val Ξ“ -> Prop
P_e: forall Ξ“ : t_ctx, ev_ctx Ξ“ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ“: t_ctx
v: val Ξ“
Ο€: ev_ctx Ξ“
IHΟ€: P_e Ξ“ Ο€
P_e Ξ“ (K2 v Ο€)
 apply (ind_karg _ _ _ H); auto; apply (val_ind_mut _ _ _ H).
Qed.

Renaming respects pointwise equality of assignments.

Definition t_ren_proper_P Ξ“ (t : term Ξ“) : Prop :=
  forall Ξ” (f1 f2 : Ξ“ βŠ† Ξ”), f1 ≑ₐ f2 -> t β‚œβŠ›α΅£ f1 = t β‚œβŠ›α΅£ f2 .
Definition v_ren_proper_P Ξ“ (v : val Ξ“) : Prop :=
  forall Ξ” (f1 f2 : Ξ“ βŠ† Ξ”), f1 ≑ₐ f2 -> v α΅₯βŠ›α΅£ f1 = v α΅₯βŠ›α΅£ f2 .
Definition e_ren_proper_P Ξ“ (Ο€ : ev_ctx Ξ“) : Prop :=
  forall Ξ” (f1 f2 : Ξ“ βŠ† Ξ”), f1 ≑ₐ f2 -> Ο€ β‚‘βŠ›α΅£ f1 = Ο€ β‚‘βŠ›α΅£ f2 .

syn_ind_args t_ren_proper_P v_ren_proper_P
  e_ren_proper_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_proper_P Ξ“ v -> t_ren_proper_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_ren_proper_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_ren_proper_P Ξ“ t2 -> t_ren_proper_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•),
v_ren_proper_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_ren_proper_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_ren_proper_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–),
e_ren_proper_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_ren_proper_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_ren_proper_P Ξ“ Ο€ -> e_ren_proper_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_proper_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_ren_proper_P Ξ“ Ο€ -> e_ren_proper_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> v α΅₯βŠ›α΅£ f1 = v α΅₯βŠ›α΅£ f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> Val v β‚œβŠ›α΅£ f1 = Val v β‚œβŠ›α΅£ f2
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> t1 β‚œβŠ›α΅£ f1 = t1 β‚œβŠ›α΅£ f2) ->
forall t2 : term Ξ“,
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> t2 β‚œβŠ›α΅£ f1 = t2 β‚œβŠ›α΅£ f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> App t1 t2 β‚œβŠ›α΅£ f1 = App t1 t2 β‚œβŠ›α΅£ f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•) (Ξ” : t_ctx)
  (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> Var i α΅₯βŠ›α΅£ f1 = Var i α΅₯βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
(forall (Ξ” : t_ctx) (f1 f2 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ”),
 f1 ≑ₐ f2 -> t β‚œβŠ›α΅£ f1 = t β‚œβŠ›α΅£ f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> Lam t α΅₯βŠ›α΅£ f1 = Lam t α΅₯βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–) (Ξ” : t_ctx)
  (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> K0 i β‚‘βŠ›α΅£ f1 = K0 i β‚‘βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (t : term Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> t β‚œβŠ›α΅£ f1 = t β‚œβŠ›α΅£ f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> Ο€ β‚‘βŠ›α΅£ f1 = Ο€ β‚‘βŠ›α΅£ f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> K1 t Ο€ β‚‘βŠ›α΅£ f1 = K1 t Ο€ β‚‘βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> v α΅₯βŠ›α΅£ f1 = v α΅₯βŠ›α΅£ f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
 f1 ≑ₐ f2 -> Ο€ β‚‘βŠ›α΅£ f1 = Ο€ β‚‘βŠ›α΅£ f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ βŠ† Ξ”),
f1 ≑ₐ f2 -> K2 v Ο€ β‚‘βŠ›α΅£ f1 = K2 v Ο€ β‚‘βŠ›α΅£ f2

  
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ•
Ξ”: t_ctx
f1, f2: Ξ“ βŠ† Ξ”
H: f1 ≑ₐ f2
f1 (βŠ•) i = f2 (βŠ•) i
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ” : t_ctx) (f1 f2 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ”),
f1 ≑ₐ f2 -> t β‚œβŠ›α΅£ f1 = t β‚œβŠ›α΅£ f2
Ξ”: t_ctx
f1, f2: Ξ“ βŠ† Ξ”
H0: f1 ≑ₐ f2
t β‚œβŠ›α΅£ r_shift1 f1 = t β‚œβŠ›α΅£ r_shift1 f2
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ–
Ξ”: t_ctx
f1, f2: Ξ“ βŠ† Ξ”
H: f1 ≑ₐ f2
f1 (βŠ–) i = f2 (βŠ–) i

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ” : t_ctx) (f1 f2 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ”),
f1 ≑ₐ f2 -> t β‚œβŠ›α΅£ f1 = t β‚œβŠ›α΅£ f2
Ξ”: t_ctx
f1, f2: Ξ“ βŠ† Ξ”
H0: f1 ≑ₐ f2
r_shift1 f1 ≑ₐ r_shift1 f2

  now apply r_shift1_eq.
Qed.


Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) t_rename

  intros f1 f2 H1 x y ->; now apply (term_ind_mut _ _ _ ren_proper_prf).
Qed.

Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) v_rename

  intros f1 f2 H1 x y ->; now apply (val_ind_mut _ _ _ ren_proper_prf).
Qed.

Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) e_rename

  intros f1 f2 H1 x y ->; now apply (ctx_ind_mut _ _ _ ren_proper_prf).
Qed.

Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> (βˆ€β‚• a, eq ==> eq)) m_rename

  intros ? ? H1 [] _ ? ->; cbn in *; now rewrite H1.
Qed.

Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) s_rename

  intros ? ? H1 _ x ->; destruct x; cbn; now rewrite H1.
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
Proper
  (asgn_eq Ξ“1 Ξ“2 ==> asgn_eq Ξ“2 Ξ“3 ==> asgn_eq Ξ“1 Ξ“3)
  a_ren

  intros ?? H1 ?? H2 ??; apply (m_ren_eq _ _ H2), H1.
Qed.

Ξ“, Ξ”: t_ctx
x: ty
Proper (asgn_eq Ξ“ Ξ” ==> asgn_eq (Ξ“ β–Άβ‚“ x) (Ξ” β–Άβ‚“ x))
  a_shift1

  
Ξ“1: ctx ty
Ξ”: t_ctx
y0: ty
x0, y: Ξ“1 =[ val_m ]> Ξ”
H: x0 ≑ₐ y
a: ty
v: var a Ξ“1
m_shift1 a (x0 a v) = m_shift1 a (y a v)

  now rewrite H.
Qed.

Renaming-renaming assocativity.

Definition t_ren_ren_P Ξ“1 (t : term Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
    (t β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)  .
Definition v_ren_ren_P Ξ“1 (v : val Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
    (v α΅₯βŠ›α΅£ f1) α΅₯βŠ›α΅£ f2 = v α΅₯βŠ›α΅£ (f1 α΅£βŠ› f2)  .
Definition e_ren_ren_P Ξ“1 (Ο€ : ev_ctx Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
    (Ο€ β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = Ο€ β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)  .


syn_ind_args t_ren_ren_P v_ren_ren_P e_ren_ren_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_ren_P Ξ“ v -> t_ren_ren_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_ren_ren_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_ren_ren_P Ξ“ t2 -> t_ren_ren_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), v_ren_ren_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_ren_ren_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_ren_ren_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), e_ren_ren_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_ren_ren_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_ren_ren_P Ξ“ Ο€ -> e_ren_ren_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_ren_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_ren_ren_P Ξ“ Ο€ -> e_ren_ren_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (v α΅₯βŠ›α΅£ f1) α΅₯βŠ›α΅£ f2 = v α΅₯βŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(Val v β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = Val v β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (t1 β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t1 β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall t2 : term Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (t2 β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t2 β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(App t1 t2 β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = App t1 t2 β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(Var i α΅₯βŠ›α΅£ f1) α΅₯βŠ›α΅£ f2 = Var i α΅₯βŠ›α΅£ (f1 α΅£βŠ› f2)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3),
 (t β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(Lam t α΅₯βŠ›α΅£ f1) α΅₯βŠ›α΅£ f2 = Lam t α΅₯βŠ›α΅£ (f1 α΅£βŠ› f2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(K0 i β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = K0 i β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)
forall (Ξ“ : t_ctx) (t : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (t β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (Ο€ β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = Ο€ β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(K1 t Ο€ β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = K1 t Ο€ β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (v α΅₯βŠ›α΅£ f1) α΅₯βŠ›α΅£ f2 = v α΅₯βŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
 (Ο€ β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = Ο€ β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(K2 v Ο€ β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = K2 v Ο€ β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(t β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)
Ξ“2, Ξ“3: t_ctx
f1: Ξ“ βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
(t β‚œβŠ›α΅£ r_shift1 f1) β‚œβŠ›α΅£ r_shift1 f2 =
t β‚œβŠ›α΅£ r_shift1 (f1 α΅£βŠ› f2)

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(t β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)
Ξ“2, Ξ“3: t_ctx
f1: Ξ“ βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
r_shift1 f1 α΅£βŠ› r_shift1 f2 ≑ₐ r_shift1 (f1 α΅£βŠ› f2)

  intros ? h; dependent elimination h; auto.
Qed.


Ξ“1, Ξ“2, Ξ“3: ctx ty
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
t: term Ξ“1
(t β‚œβŠ›α΅£ f1) β‚œβŠ›α΅£ f2 = t β‚œβŠ›α΅£ (f1 α΅£βŠ› f2)

  now apply (term_ind_mut _ _ _ ren_ren_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: ctx ty
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
v: val Ξ“1
(v α΅₯βŠ›α΅£ f1) α΅₯βŠ›α΅£ f2 = v α΅₯βŠ›α΅£ (f1 α΅£βŠ› f2)

  now apply (val_ind_mut _ _ _ ren_ren_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: ctx ty
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
Ο€: ev_ctx Ξ“1
(Ο€ β‚‘βŠ›α΅£ f1) β‚‘βŠ›α΅£ f2 = Ο€ β‚‘βŠ›α΅£ (f1 α΅£βŠ› f2)

  now apply (ctx_ind_mut _ _ _ ren_ren_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: ctx ty
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a: ty
v: val_m Ξ“1 a
(v β‚˜βŠ›α΅£ f1) β‚˜βŠ›α΅£ f2 = v β‚˜βŠ›α΅£ (f1 α΅£βŠ› f2)

  destruct a; [ now apply v_ren_ren | now apply e_ren_ren ].
Qed.

Ξ“1, Ξ“2, Ξ“3: ctx ty
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 βŠ† Ξ“3
s: state Ξ“1
(s β‚›βŠ›α΅£ f1) β‚›βŠ›α΅£ f2 = s β‚›βŠ›α΅£ (f1 α΅£βŠ› f2)

  destruct s; apply (f_equal2 Cut); [ now apply t_ren_ren | now apply e_ren_ren ].
Qed.

Left identity law of renaming.

Definition t_ren_id_l_P Ξ“ (t : term Ξ“) : Prop := t β‚œβŠ›α΅£ r_id = t .
Definition v_ren_id_l_P Ξ“ (v : val Ξ“) : Prop := v α΅₯βŠ›α΅£ r_id = v .
Definition e_ren_id_l_P Ξ“ (Ο€ : ev_ctx Ξ“) : Prop := Ο€ β‚‘βŠ›α΅£ r_id = Ο€ .

syn_ind_args t_ren_id_l_P v_ren_id_l_P e_ren_id_l_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_id_l_P Ξ“ v -> t_ren_id_l_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_ren_id_l_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_ren_id_l_P Ξ“ t2 -> t_ren_id_l_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), v_ren_id_l_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_ren_id_l_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_ren_id_l_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), e_ren_id_l_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_ren_id_l_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_ren_id_l_P Ξ“ Ο€ -> e_ren_id_l_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_id_l_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_ren_id_l_P Ξ“ Ο€ -> e_ren_id_l_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v α΅₯βŠ›α΅£ r_id = v -> Val v β‚œβŠ›α΅£ r_id = Val v
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t1 β‚œβŠ›α΅£ r_id = t1 ->
forall t2 : term Ξ“,
t2 β‚œβŠ›α΅£ r_id = t2 -> App t1 t2 β‚œβŠ›α΅£ r_id = App t1 t2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), Var i α΅₯βŠ›α΅£ r_id = Var i
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t β‚œβŠ›α΅£ r_id = t -> Lam t α΅₯βŠ›α΅£ r_id = Lam t
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), K0 i β‚‘βŠ›α΅£ r_id = K0 i
forall (Ξ“ : t_ctx) (t : term Ξ“),
t β‚œβŠ›α΅£ r_id = t ->
forall Ο€ : ev_ctx Ξ“,
Ο€ β‚‘βŠ›α΅£ r_id = Ο€ -> K1 t Ο€ β‚‘βŠ›α΅£ r_id = K1 t Ο€
forall (Ξ“ : t_ctx) (v : val Ξ“),
v α΅₯βŠ›α΅£ r_id = v ->
forall Ο€ : ev_ctx Ξ“,
Ο€ β‚‘βŠ›α΅£ r_id = Ο€ -> K2 v Ο€ β‚‘βŠ›α΅£ r_id = K2 v Ο€

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: t β‚œβŠ›α΅£ r_id = t
t β‚œβŠ›α΅£ r_shift1 r_id = t

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: t β‚œβŠ›α΅£ r_id = t
r_shift1 r_id ≑ₐ r_id

  intros ? h; dependent elimination h; auto.
Qed.


Ξ“: t_ctx
t: term Ξ“
t β‚œβŠ›α΅£ r_id = t

  now apply (term_ind_mut _ _ _ ren_id_l_prf).
Qed.

Ξ“: t_ctx
v: val Ξ“
v α΅₯βŠ›α΅£ r_id = v

  now apply (val_ind_mut _ _ _ ren_id_l_prf).
Qed.

Ξ“: t_ctx
Ο€: ev_ctx Ξ“
Ο€ β‚‘βŠ›α΅£ r_id = Ο€

  now apply (ctx_ind_mut _ _ _ ren_id_l_prf).
Qed.

Ξ“: t_ctx
a: ty
v: val_m Ξ“ a
v β‚˜βŠ›α΅£ r_id = v

  destruct a; [ now apply v_ren_id_l | now apply e_ren_id_l ].
Qed.

Ξ“: t_ctx
s: state Ξ“
s β‚›βŠ›α΅£ r_id = s

  destruct s; apply (f_equal2 Cut); [ now apply t_ren_id_l | now apply e_ren_id_l ].
Qed.


Ξ“, Ξ”: ctx ty
f: Ξ“ βŠ† Ξ”
a: ty
i: Ξ“ βˆ‹ a
a_id a i β‚˜βŠ›α΅£ f = a_id a (f a i)

  now destruct a.
Qed.


Ξ“, Ξ”: ctx ty
f: Ξ“ βŠ† Ξ”
a_id βŠ›α΅£ f ≑ₐ f α΅£βŠ› a_id

  intros ??; now apply m_ren_id_r.
Qed.

Ξ“: t_ctx
x: ty
a_shift1 a_id ≑ₐ a_id

  
Ξ“1: ctx ty
y, a: ty
v: var a Ξ“1
a_shift1 a_id a (pop v) = a_id a (pop v)

  exact (m_ren_id_r _ _).
Qed.

Lemma 5: shifting assigments commutes with left and right renaming.

Ξ“1, Ξ“2: ctx ty
Ξ“3: t_ctx
a: ty
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
a_shift1 (f1 α΅£βŠ› f2) ≑ₐ r_shift1 f1 α΅£βŠ› a_shift1 f2

  intros ? v; dependent elimination v; auto.
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
a: ty
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a_shift1 (f1 βŠ›α΅£ f2) ≑ₐ a_shift1 f1 βŠ›α΅£ r_shift1 f2

  
Ξ“1, Ξ“2, Ξ“3: t_ctx
a: ty
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a0: ty
v: Ξ“1 β–Άβ‚“ a βˆ‹ a0
a_shift1 (f1 βŠ›α΅£ f2) a0 v =
(a_shift1 f1 βŠ›α΅£ r_shift1 f2)%asgn a0 v

  
Ξ“: ctx ty
Ξ“2, Ξ“3: t_ctx
a0: ty
f1: Ξ“ =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a_shift1 (f1 βŠ›α΅£ f2) a0 top =
(a_shift1 f1 βŠ›α΅£ r_shift1 f2)%asgn a0 top
Ξ“0: ctx ty
Ξ“2, Ξ“3: t_ctx
y: ty
f1: Ξ“0 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a0: ty
v: var a0 Ξ“0
a_shift1 (f1 βŠ›α΅£ f2) a0 (pop v) =
(a_shift1 f1 βŠ›α΅£ r_shift1 f2)%asgn a0 (pop v)

  
Ξ“0: ctx ty
Ξ“2, Ξ“3: t_ctx
y: ty
f1: Ξ“0 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a0: ty
v: var a0 Ξ“0
a_shift1 (f1 βŠ›α΅£ f2) a0 (pop v) =
(a_shift1 f1 βŠ›α΅£ r_shift1 f2)%asgn a0 (pop v)

  cbn; unfold m_shift1, r_shift1; now rewrite 2 m_ren_ren.
Qed.

Lemma 6: substitution respects pointwise equality of assigments.

Definition t_sub_proper_P Ξ“ (t : term Ξ“) : Prop :=
  forall Ξ” (f1 f2 : Ξ“ =[val_m]> Ξ”), f1 ≑ₐ f2 -> t `β‚œβŠ› f1 = t `β‚œβŠ› f2 .
Definition v_sub_proper_P Ξ“ (v : val Ξ“) : Prop :=
  forall Ξ” (f1 f2 : Ξ“ =[val_m]> Ξ”), f1 ≑ₐ f2 -> v `α΅₯βŠ› f1 = v `α΅₯βŠ› f2 .
Definition e_sub_proper_P Ξ“ (Ο€ : ev_ctx Ξ“) : Prop :=
  forall Ξ” (f1 f2 : Ξ“ =[val_m]> Ξ”), f1 ≑ₐ f2 -> Ο€ `β‚‘βŠ› f1 = Ο€ `β‚‘βŠ› f2.

syn_ind_args t_sub_proper_P v_sub_proper_P
  e_sub_proper_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_proper_P Ξ“ v -> t_sub_proper_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_sub_proper_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_sub_proper_P Ξ“ t2 -> t_sub_proper_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•),
v_sub_proper_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_sub_proper_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_sub_proper_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–),
e_sub_proper_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_sub_proper_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_sub_proper_P Ξ“ Ο€ -> e_sub_proper_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_proper_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_sub_proper_P Ξ“ Ο€ -> e_sub_proper_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> v `α΅₯βŠ› f1 = v `α΅₯βŠ› f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> Val v `β‚œβŠ› f1 = Val v `β‚œβŠ› f2
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> t1 `β‚œβŠ› f1 = t1 `β‚œβŠ› f2) ->
forall t2 : term Ξ“,
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> t2 `β‚œβŠ› f1 = t2 `β‚œβŠ› f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> App t1 t2 `β‚œβŠ› f1 = App t1 t2 `β‚œβŠ› f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•) (Ξ” : t_ctx)
  (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> Var i `α΅₯βŠ› f1 = Var i `α΅₯βŠ› f2
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
(forall (Ξ” : t_ctx) (f1 f2 : (Ξ“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> t `β‚œβŠ› f1 = t `β‚œβŠ› f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> Lam t `α΅₯βŠ› f1 = Lam t `α΅₯βŠ› f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–) (Ξ” : t_ctx)
  (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> K0 i `β‚‘βŠ› f1 = K0 i `β‚‘βŠ› f2
forall (Ξ“ : t_ctx) (t : term Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> t `β‚œβŠ› f1 = t `β‚œβŠ› f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> Ο€ `β‚‘βŠ› f1 = Ο€ `β‚‘βŠ› f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> K1 t Ο€ `β‚‘βŠ› f1 = K1 t Ο€ `β‚‘βŠ› f2
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> v `α΅₯βŠ› f1 = v `α΅₯βŠ› f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
 f1 ≑ₐ f2 -> Ο€ `β‚‘βŠ› f1 = Ο€ `β‚‘βŠ› f2) ->
forall (Ξ” : t_ctx) (f1 f2 : Ξ“ =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> K2 v Ο€ `β‚‘βŠ› f1 = K2 v Ο€ `β‚‘βŠ› f2

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ” : t_ctx)
  (f1 f2 : (Ξ“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ”),
f1 ≑ₐ f2 -> t `β‚œβŠ› f1 = t `β‚œβŠ› f2
Ξ”: t_ctx
f1, f2: Ξ“ =[ val_m ]> Ξ”
H0: f1 ≑ₐ f2
t `β‚œβŠ› a_shift1 f1 = t `β‚œβŠ› a_shift1 f2

  now apply H, a_shift_eq.
Qed.


Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) t_subst

  intros ? ? H1 _ ? ->; now apply (term_ind_mut _ _ _ sub_proper_prf).
Qed.

Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) v_subst

  intros ? ? H1 _ ? ->; now apply (val_ind_mut _ _ _ sub_proper_prf).
Qed.

Ξ“, Ξ”: t_ctx
Proper (asgn_eq Ξ“ Ξ” ==> eq ==> eq) e_subst

  intros ? ? H1 _ ? ->; now apply (ctx_ind_mut _ _ _ sub_proper_prf).
Qed.

Proper
  (βˆ€β‚• Ξ“, (βˆ€β‚• a, eq ==> (βˆ€β‚• Ξ”, asgn_eq Ξ“ Ξ” ==> eq)))
  m_subst

  intros ? [] ?? -> ??? H1; cbn in *; now rewrite H1.
Qed.

Proper (βˆ€β‚• Ξ“, eq ==> (βˆ€β‚• Ξ”, asgn_eq Ξ“ Ξ” ==> eq))
  s_subst

  intros ??[] -> ??? H1; cbn; now rewrite H1.
Qed.
(*
#[global] Instance a_comp_eq {Ξ“1 Ξ“2 Ξ“3} : Proper (ass_eq _ _ ==> ass_eq _ _ ==> ass_eq _ _) (@a_comp Ξ“1 Ξ“2 Ξ“3).
  intros ? ? H1 ? ? H2 ? ?; unfold a_comp, s_map; now rewrite H1, H2.
Qed.
*)

Lemma 7: renaming-substitution "associativity".

Definition t_ren_sub_P Ξ“1 (t : term Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 =[val_m]> Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3) ,
    (t `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t `β‚œβŠ› (f1 βŠ›α΅£ f2) .
Definition v_ren_sub_P Ξ“1 (v : val Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 =[val_m]> Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3) ,
    (v `α΅₯βŠ› f1) α΅₯βŠ›α΅£ f2 = v `α΅₯βŠ› (f1 βŠ›α΅£ f2) .
Definition e_ren_sub_P Ξ“1 (Ο€ : ev_ctx Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 =[val_m]> Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3) ,
    (Ο€ `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = Ο€ `β‚‘βŠ› (f1 βŠ›α΅£ f2) .

syn_ind_args t_ren_sub_P v_ren_sub_P e_ren_sub_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_sub_P Ξ“ v -> t_ren_sub_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_ren_sub_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_ren_sub_P Ξ“ t2 -> t_ren_sub_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), v_ren_sub_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_ren_sub_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_ren_sub_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), e_ren_sub_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_ren_sub_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_ren_sub_P Ξ“ Ο€ -> e_ren_sub_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_ren_sub_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_ren_sub_P Ξ“ Ο€ -> e_ren_sub_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3), (v `α΅₯βŠ› f1) α΅₯βŠ›α΅£ f2 = v `α΅₯βŠ› f1 βŠ›α΅£ f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(Val v `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = Val v `β‚œβŠ› f1 βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3),
 (t1 `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t1 `β‚œβŠ› f1 βŠ›α΅£ f2) ->
forall t2 : term Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3),
 (t2 `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t2 `β‚œβŠ› f1 βŠ›α΅£ f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(App t1 t2 `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = App t1 t2 `β‚œβŠ› f1 βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ =[ val_m ]> Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(Var i `α΅₯βŠ› f1) α΅₯βŠ›α΅£ f2 = Var i `α΅₯βŠ› f1 βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3), (t `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t `β‚œβŠ› f1 βŠ›α΅£ f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(Lam t `α΅₯βŠ› f1) α΅₯βŠ›α΅£ f2 = Lam t `α΅₯βŠ› f1 βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ =[ val_m ]> Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(K0 i `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = K0 i `β‚‘βŠ› f1 βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (t : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3), (t `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t `β‚œβŠ› f1 βŠ›α΅£ f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3), (Ο€ `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = Ο€ `β‚‘βŠ› f1 βŠ›α΅£ f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(K1 t Ο€ `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = K1 t Ο€ `β‚‘βŠ› f1 βŠ›α΅£ f2
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3), (v `α΅₯βŠ› f1) α΅₯βŠ›α΅£ f2 = v `α΅₯βŠ› f1 βŠ›α΅£ f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 βŠ† Ξ“3), (Ο€ `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = Ο€ `β‚‘βŠ› f1 βŠ›α΅£ f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 βŠ† Ξ“3),
(K2 v Ο€ `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = K2 v Ο€ `β‚‘βŠ› f1 βŠ›α΅£ f2

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ“2 Ξ“3 : t_ctx)
  (f1 : (Ξ“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“2) (f2 : Ξ“2 βŠ† Ξ“3),
(t `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t `β‚œβŠ› f1 βŠ›α΅£ f2
Ξ“2, Ξ“3: t_ctx
f1: Ξ“ =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
(t `β‚œβŠ› a_shift1 f1) β‚œβŠ›α΅£ r_shift1 f2 =
t `β‚œβŠ› a_shift1 (fun x : ty => m_rename f2 x ∘ f1 x)

  change (a_shift1 (fun x => _)) with (a_shift1 (a:=βŠ•) (f1 βŠ›α΅£ f2)); now rewrite a_shift1_a_ren.
Qed.


Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
t: term Ξ“1
(t `β‚œβŠ› f1) β‚œβŠ›α΅£ f2 = t `β‚œβŠ› f1 βŠ›α΅£ f2

  now apply (term_ind_mut _ _ _ ren_sub_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
v: val Ξ“1
(v `α΅₯βŠ› f1) α΅₯βŠ›α΅£ f2 = v `α΅₯βŠ› f1 βŠ›α΅£ f2

  now apply (val_ind_mut _ _ _ ren_sub_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
Ο€: ev_ctx Ξ“1
(Ο€ `β‚‘βŠ› f1) β‚‘βŠ›α΅£ f2 = Ο€ `β‚‘βŠ› f1 βŠ›α΅£ f2

  now apply (ctx_ind_mut _ _ _ ren_sub_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
a: ty
v: val_m Ξ“1 a
(v α΅₯βŠ› f1) β‚˜βŠ›α΅£ f2 = v α΅₯βŠ› f1 βŠ›α΅£ f2

  destruct a; [ now apply v_ren_sub | now apply e_ren_sub ].
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 βŠ† Ξ“3
s: state Ξ“1
(s β‚œβŠ› f1) β‚›βŠ›α΅£ f2 = s β‚œβŠ› f1 βŠ›α΅£ f2

  destruct s; cbn; now rewrite t_ren_sub, e_ren_sub.
Qed.

Lemma 8: substitution-renaming "associativity".

Definition t_sub_ren_P Ξ“1 (t : term Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 βŠ† Ξ“2) (f2 : Ξ“2 =[val_m]> Ξ“3) ,
  (t β‚œβŠ›α΅£ f1) `β‚œβŠ› f2 = t `β‚œβŠ› (f1 α΅£βŠ› f2) .
Definition v_sub_ren_P Ξ“1 (v : val Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 βŠ† Ξ“2) (f2 : Ξ“2 =[val_m]> Ξ“3) ,
  (v α΅₯βŠ›α΅£ f1) `α΅₯βŠ› f2 = v `α΅₯βŠ› (f1 α΅£βŠ› f2) .
Definition e_sub_ren_P Ξ“1 (Ο€ : ev_ctx Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 βŠ† Ξ“2) (f2 : Ξ“2 =[val_m]> Ξ“3) ,
  (Ο€ β‚‘βŠ›α΅£ f1) `β‚‘βŠ› f2 = Ο€ `β‚‘βŠ› (f1 α΅£βŠ› f2) .

syn_ind_args t_sub_ren_P v_sub_ren_P e_sub_ren_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_ren_P Ξ“ v -> t_sub_ren_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_sub_ren_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_sub_ren_P Ξ“ t2 -> t_sub_ren_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), v_sub_ren_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_sub_ren_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_sub_ren_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), e_sub_ren_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_sub_ren_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_sub_ren_P Ξ“ Ο€ -> e_sub_ren_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_ren_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_sub_ren_P Ξ“ Ο€ -> e_sub_ren_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 v α΅₯βŠ›α΅£ f1 `α΅₯βŠ› f2 = v `α΅₯βŠ› f1 α΅£βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
Val v β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = Val v `β‚œβŠ› f1 α΅£βŠ› f2
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t1 β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = t1 `β‚œβŠ› f1 α΅£βŠ› f2) ->
forall t2 : term Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t2 β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = t2 `β‚œβŠ› f1 α΅£βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
App t1 t2 β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = App t1 t2 `β‚œβŠ› f1 α΅£βŠ› f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 =[ val_m ]> Ξ“3),
Var i α΅₯βŠ›α΅£ f1 `α΅₯βŠ› f2 = Var i `α΅₯βŠ› f1 α΅£βŠ› f2
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = t `β‚œβŠ› f1 α΅£βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
Lam t α΅₯βŠ›α΅£ f1 `α΅₯βŠ› f2 = Lam t `α΅₯βŠ› f1 α΅£βŠ› f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ βŠ† Ξ“2) (f2 : Ξ“2 =[ val_m ]> Ξ“3),
K0 i β‚‘βŠ›α΅£ f1 `β‚‘βŠ› f2 = K0 i `β‚‘βŠ› f1 α΅£βŠ› f2
forall (Ξ“ : t_ctx) (t : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = t `β‚œβŠ› f1 α΅£βŠ› f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 Ο€ β‚‘βŠ›α΅£ f1 `β‚‘βŠ› f2 = Ο€ `β‚‘βŠ› f1 α΅£βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
K1 t Ο€ β‚‘βŠ›α΅£ f1 `β‚‘βŠ› f2 = K1 t Ο€ `β‚‘βŠ› f1 α΅£βŠ› f2
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 v α΅₯βŠ›α΅£ f1 `α΅₯βŠ› f2 = v `α΅₯βŠ› f1 α΅£βŠ› f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 Ο€ β‚‘βŠ›α΅£ f1 `β‚‘βŠ› f2 = Ο€ `β‚‘βŠ› f1 α΅£βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ βŠ† Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
K2 v Ο€ β‚‘βŠ›α΅£ f1 `β‚‘βŠ› f2 = K2 v Ο€ `β‚‘βŠ› f1 α΅£βŠ› f2

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) βŠ† Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
t β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = t `β‚œβŠ› f1 α΅£βŠ› f2
Ξ“2, Ξ“3: t_ctx
f1: Ξ“ βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
t β‚œβŠ›α΅£ r_shift1 f1 `β‚œβŠ› a_shift1 f2 =
t `β‚œβŠ› a_shift1 (f1 α΅£βŠ› f2)

  now rewrite a_shift1_s_ren.
Qed.


Ξ“1, Ξ“2: ctx ty
Ξ“3: t_ctx
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
t: term Ξ“1
t β‚œβŠ›α΅£ f1 `β‚œβŠ› f2 = t `β‚œβŠ› f1 α΅£βŠ› f2

  now apply (term_ind_mut _ _ _ sub_ren_prf).
Qed.

Ξ“1, Ξ“2: ctx ty
Ξ“3: t_ctx
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
v: val Ξ“1
v α΅₯βŠ›α΅£ f1 `α΅₯βŠ› f2 = v `α΅₯βŠ› f1 α΅£βŠ› f2

  now apply (val_ind_mut _ _ _ sub_ren_prf).
Qed.

Ξ“1, Ξ“2: ctx ty
Ξ“3: t_ctx
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
Ο€: ev_ctx Ξ“1
Ο€ β‚‘βŠ›α΅£ f1 `β‚‘βŠ› f2 = Ο€ `β‚‘βŠ› f1 α΅£βŠ› f2

  now apply (ctx_ind_mut _ _ _ sub_ren_prf).
Qed.

Ξ“1, Ξ“2: ctx ty
Ξ“3: t_ctx
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
a: ty
v: val_m Ξ“1 a
v β‚˜βŠ›α΅£ f1 α΅₯βŠ› f2 = v α΅₯βŠ› f1 α΅£βŠ› f2

  destruct a; [ now apply v_sub_ren | now apply e_sub_ren ].
Qed.

Ξ“1, Ξ“2: ctx ty
Ξ“3: t_ctx
f1: Ξ“1 βŠ† Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
s: state Ξ“1
s β‚›βŠ›α΅£ f1 β‚œβŠ› f2 = s β‚œβŠ› f1 α΅£βŠ› f2

  destruct s; cbn; now rewrite t_sub_ren, e_sub_ren.
Qed.

Lemma 9: left identity law of substitution.

Definition t_sub_id_l_P Ξ“ (t : term Ξ“) : Prop := t `β‚œβŠ› a_id = t .
Definition v_sub_id_l_P Ξ“ (v : val Ξ“) : Prop := v `α΅₯βŠ› a_id = v .
Definition e_sub_id_l_P Ξ“ (Ο€ : ev_ctx Ξ“) : Prop := Ο€ `β‚‘βŠ› a_id = Ο€ .

syn_ind_args t_sub_id_l_P v_sub_id_l_P e_sub_id_l_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_id_l_P Ξ“ v -> t_sub_id_l_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_sub_id_l_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_sub_id_l_P Ξ“ t2 -> t_sub_id_l_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), v_sub_id_l_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_sub_id_l_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_sub_id_l_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), e_sub_id_l_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_sub_id_l_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_sub_id_l_P Ξ“ Ο€ -> e_sub_id_l_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_id_l_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_sub_id_l_P Ξ“ Ο€ -> e_sub_id_l_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v `α΅₯βŠ› a_id = v -> Val v `β‚œβŠ› a_id = Val v
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t1 `β‚œβŠ› a_id = t1 ->
forall t2 : term Ξ“,
t2 `β‚œβŠ› a_id = t2 -> App t1 t2 `β‚œβŠ› a_id = App t1 t2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), Var i `α΅₯βŠ› a_id = Var i
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t `β‚œβŠ› a_id = t -> Lam t `α΅₯βŠ› a_id = Lam t
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), K0 i `β‚‘βŠ› a_id = K0 i
forall (Ξ“ : t_ctx) (t : term Ξ“),
t `β‚œβŠ› a_id = t ->
forall Ο€ : ev_ctx Ξ“,
Ο€ `β‚‘βŠ› a_id = Ο€ -> K1 t Ο€ `β‚‘βŠ› a_id = K1 t Ο€
forall (Ξ“ : t_ctx) (v : val Ξ“),
v `α΅₯βŠ› a_id = v ->
forall Ο€ : ev_ctx Ξ“,
Ο€ `β‚‘βŠ› a_id = Ο€ -> K2 v Ο€ `β‚‘βŠ› a_id = K2 v Ο€

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: t `β‚œβŠ› a_id = t
t `β‚œβŠ› a_shift1 a_id = t

  now rewrite a_shift_id.
Qed.


Ξ“: t_ctx
t: term Ξ“
t `β‚œβŠ› a_id = t

  now apply (term_ind_mut _ _ _ sub_id_l_prf).
Qed.

Ξ“: t_ctx
v: val Ξ“
v `α΅₯βŠ› a_id = v

  now apply (val_ind_mut _ _ _ sub_id_l_prf).
Qed.

Ξ“: t_ctx
Ο€: ev_ctx Ξ“
Ο€ `β‚‘βŠ› a_id = Ο€

  now apply (ctx_ind_mut _ _ _ sub_id_l_prf).
Qed.

Ξ“: t_ctx
a: ty
v: val_m Ξ“ a
v α΅₯βŠ› a_id = v

  destruct a; [ now apply v_sub_id_l | now apply e_sub_id_l ].
Qed.

Ξ“: t_ctx
s: state Ξ“
s β‚œβŠ› a_id = s

  destruct s; cbn; now rewrite t_sub_id_l, e_sub_id_l.
Qed.

Lemma 9: right identity law of substitution. As for renaming, this one is mostly by definition.

Ξ“1: ctx ty
Ξ“2: t_ctx
a: ty
i: Ξ“1 βˆ‹ a
f: Ξ“1 =[ val_m ]> Ξ“2
a_id a i α΅₯βŠ› f = f a i

  now destruct a.
Qed.

Lemma 10: shifting assigments respects composition.

Ξ“1, Ξ“2, Ξ“3: t_ctx
a: ty
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
a_shift1 (f1 βŠ› f2) ≑ₐ a_shift1 f1 βŠ› a_shift1 f2

  
Ξ“: ctx ty
Ξ“2, Ξ“3: t_ctx
a0: ty
f1: Ξ“ =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
a_id a0 top =
m_subst (Ξ“2 β–Άβ‚“ a0) a0 (a_id a0 top) (Ξ“3 β–Άβ‚“ a0)
  (a_shift1 f2)
Ξ“0: ctx ty
Ξ“2, Ξ“3: t_ctx
y: ty
f1: Ξ“0 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
a0: ty
v: var a0 Ξ“0
m_shift1 a0 (m_subst Ξ“2 a0 (f1 a0 v) Ξ“3 f2) =
m_subst (Ξ“2 β–Άβ‚“ y) a0 (m_shift1 a0 (f1 a0 v)) (Ξ“3 β–Άβ‚“ y)
  (a_shift1 f2)

  
Ξ“0: ctx ty
Ξ“2, Ξ“3: t_ctx
y: ty
f1: Ξ“0 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
a0: ty
v: var a0 Ξ“0
m_shift1 a0 (m_subst Ξ“2 a0 (f1 a0 v) Ξ“3 f2) =
m_subst (Ξ“2 β–Άβ‚“ y) a0 (m_shift1 a0 (f1 a0 v)) (Ξ“3 β–Άβ‚“ y)
  (a_shift1 f2)

  unfold m_shift1; now rewrite m_ren_sub, m_sub_ren.
Qed.

Lemma 11: substitution-substitution associativity, ie composition law.

Definition t_sub_sub_P Ξ“1 (t : term Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 =[val_m]> Ξ“2) (f2 : Ξ“2 =[val_m]> Ξ“3) ,
  t `β‚œβŠ› (f1 βŠ› f2) = (t `β‚œβŠ› f1) `β‚œβŠ› f2 .
Definition v_sub_sub_P Ξ“1 (v : val Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 =[val_m]> Ξ“2) (f2 : Ξ“2 =[val_m]> Ξ“3) ,
  v `α΅₯βŠ› (f1 βŠ› f2) = (v `α΅₯βŠ› f1) `α΅₯βŠ› f2 .
Definition e_sub_sub_P Ξ“1 (Ο€ : ev_ctx Ξ“1) : Prop :=
  forall Ξ“2 Ξ“3 (f1 : Ξ“1 =[val_m]> Ξ“2) (f2 : Ξ“2 =[val_m]> Ξ“3) ,
  Ο€ `β‚‘βŠ› (f1 βŠ› f2) = (Ο€ `β‚‘βŠ› f1) `β‚‘βŠ› f2 .

syn_ind_args t_sub_sub_P v_sub_sub_P e_sub_sub_P

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_sub_P Ξ“ v -> t_sub_sub_P Ξ“ (Val v)
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
t_sub_sub_P Ξ“ t1 ->
forall t2 : term Ξ“,
t_sub_sub_P Ξ“ t2 -> t_sub_sub_P Ξ“ (App t1 t2)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•), v_sub_sub_P Ξ“ (Var i)
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
t_sub_sub_P (Ξ“ β–Άβ‚“ βŠ•) t -> v_sub_sub_P Ξ“ (Lam t)
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–), e_sub_sub_P Ξ“ (K0 i)
forall (Ξ“ : t_ctx) (t : term Ξ“),
t_sub_sub_P Ξ“ t ->
forall Ο€ : ev_ctx Ξ“,
e_sub_sub_P Ξ“ Ο€ -> e_sub_sub_P Ξ“ (K1 t Ο€)
forall (Ξ“ : t_ctx) (v : val Ξ“),
v_sub_sub_P Ξ“ v ->
forall Ο€ : ev_ctx Ξ“,
e_sub_sub_P Ξ“ Ο€ -> e_sub_sub_P Ξ“ (K2 v Ο€)

  
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 v `α΅₯βŠ› f1 βŠ› f2 = (v `α΅₯βŠ› f1) `α΅₯βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
Val v `β‚œβŠ› f1 βŠ› f2 = (Val v `β‚œβŠ› f1) `β‚œβŠ› f2
forall (Ξ“ : t_ctx) (t1 : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t1 `β‚œβŠ› f1 βŠ› f2 = (t1 `β‚œβŠ› f1) `β‚œβŠ› f2) ->
forall t2 : term Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t2 `β‚œβŠ› f1 βŠ› f2 = (t2 `β‚œβŠ› f1) `β‚œβŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
App t1 t2 `β‚œβŠ› f1 βŠ› f2 = (App t1 t2 `β‚œβŠ› f1) `β‚œβŠ› f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ•) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ =[ val_m ]> Ξ“2) (f2 : Ξ“2 =[ val_m ]> Ξ“3),
Var i `α΅₯βŠ› f1 βŠ› f2 = (Var i `α΅₯βŠ› f1) `α΅₯βŠ› f2
forall (Ξ“ : t_ctx) (t : term (Ξ“ β–Άβ‚“ βŠ•)),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : (Ξ“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t `β‚œβŠ› f1 βŠ› f2 = (t `β‚œβŠ› f1) `β‚œβŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
Lam t `α΅₯βŠ› f1 βŠ› f2 = (Lam t `α΅₯βŠ› f1) `α΅₯βŠ› f2
forall (Ξ“ : t_ctx) (i : Ξ“ βˆ‹ βŠ–) (Ξ“2 Ξ“3 : t_ctx)
  (f1 : Ξ“ =[ val_m ]> Ξ“2) (f2 : Ξ“2 =[ val_m ]> Ξ“3),
K0 i `β‚‘βŠ› f1 βŠ› f2 = (K0 i `β‚‘βŠ› f1) `β‚‘βŠ› f2
forall (Ξ“ : t_ctx) (t : term Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 t `β‚œβŠ› f1 βŠ› f2 = (t `β‚œβŠ› f1) `β‚œβŠ› f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 Ο€ `β‚‘βŠ› f1 βŠ› f2 = (Ο€ `β‚‘βŠ› f1) `β‚‘βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
K1 t Ο€ `β‚‘βŠ› f1 βŠ› f2 = (K1 t Ο€ `β‚‘βŠ› f1) `β‚‘βŠ› f2
forall (Ξ“ : t_ctx) (v : val Ξ“),
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 v `α΅₯βŠ› f1 βŠ› f2 = (v `α΅₯βŠ› f1) `α΅₯βŠ› f2) ->
forall Ο€ : ev_ctx Ξ“,
(forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
   (f2 : Ξ“2 =[ val_m ]> Ξ“3),
 Ο€ `β‚‘βŠ› f1 βŠ› f2 = (Ο€ `β‚‘βŠ› f1) `β‚‘βŠ› f2) ->
forall (Ξ“2 Ξ“3 : t_ctx) (f1 : Ξ“ =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
K2 v Ο€ `β‚‘βŠ› f1 βŠ› f2 = (K2 v Ο€ `β‚‘βŠ› f1) `β‚‘βŠ› f2

  
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
H: forall (Ξ“2 Ξ“3 : t_ctx)
  (f1 : (Ξ“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“2)
  (f2 : Ξ“2 =[ val_m ]> Ξ“3),
t `β‚œβŠ› f1 βŠ› f2 = (t `β‚œβŠ› f1) `β‚œβŠ› f2
Ξ“2, Ξ“3: t_ctx
f1: Ξ“ =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
t `β‚œβŠ› a_shift1 (f1 βŠ› f2) =
(t `β‚œβŠ› a_shift1 f1) `β‚œβŠ› a_shift1 f2

  now rewrite a_shift1_comp.
Qed.


Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
t: term Ξ“1
t `β‚œβŠ› f1 βŠ› f2 = (t `β‚œβŠ› f1) `β‚œβŠ› f2

  now apply (term_ind_mut _ _ _ sub_sub_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
v: val Ξ“1
v `α΅₯βŠ› f1 βŠ› f2 = (v `α΅₯βŠ› f1) `α΅₯βŠ› f2

  now apply (val_ind_mut _ _ _ sub_sub_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
Ο€: ev_ctx Ξ“1
Ο€ `β‚‘βŠ› f1 βŠ› f2 = (Ο€ `β‚‘βŠ› f1) `β‚‘βŠ› f2

  now apply (ctx_ind_mut _ _ _ sub_sub_prf).
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
a: ty
v: val_m Ξ“1 a
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
v α΅₯βŠ› f1 βŠ› f2 = (v α΅₯βŠ› f1) α΅₯βŠ› f2

  destruct a; [ now apply v_sub_sub | now apply e_sub_sub ].
Qed.

Ξ“1, Ξ“2, Ξ“3: t_ctx
s: state Ξ“1
f1: Ξ“1 =[ val_m ]> Ξ“2
f2: Ξ“2 =[ val_m ]> Ξ“3
s β‚œβŠ› f1 βŠ› f2 = (s β‚œβŠ› f1) β‚œβŠ› f2

  destruct s; cbn; now rewrite t_sub_sub, e_sub_sub.
Qed.

Ξ“, Ξ”: t_ctx
a: ty
f: Ξ“ =[ val_m ]> Ξ”
v: val_m Ξ“ a
a_shift1 f βŠ› assign1 (v α΅₯βŠ› f) ≑ₐ assign1 v βŠ› f

  
Ξ“0: ctx ty
Ξ”: t_ctx
a0: ty
f: Ξ“0 =[ val_m ]> Ξ”
v: val_m Ξ“0 a0
m_subst (Ξ” β–Άβ‚“ a0) a0 (a_id a0 top) Ξ”
  (assign1 (m_subst Ξ“0 a0 v Ξ” f)) =
m_subst Ξ“0 a0 v Ξ” f
Ξ“1: ctx ty
Ξ”: t_ctx
y: ty
f: Ξ“1 =[ val_m ]> Ξ”
v: val_m Ξ“1 y
a0: ty
v0: var a0 Ξ“1
m_subst (Ξ” β–Άβ‚“ y) a0 (m_shift1 a0 (f a0 v0)) Ξ”
  (assign1 (m_subst Ξ“1 y v Ξ” f)) =
m_subst Ξ“1 a0 (a_id a0 v0) Ξ” f

  
Ξ“1: ctx ty
Ξ”: t_ctx
y: ty
f: Ξ“1 =[ val_m ]> Ξ”
v: val_m Ξ“1 y
a0: ty
v0: var a0 Ξ“1
m_subst (Ξ” β–Άβ‚“ y) a0 (m_shift1 a0 (f a0 v0)) Ξ”
  (assign1 (m_subst Ξ“1 y v Ξ” f)) =
m_subst Ξ“1 a0 (a_id a0 v0) Ξ” f

  unfold m_shift1; rewrite m_sub_ren, m_sub_id_r; now apply m_sub_id_l.
Qed.

Ξ“, Ξ”: t_ctx
x: ty
f: Ξ“ =[ val_m ]> Ξ”
t: term (Ξ“ β–Άβ‚“ x)
v: val_m Ξ“ x
t `β‚œβŠ› a_shift1 f /[ v α΅₯βŠ› f] = (t /[ v]) `β‚œβŠ› f

  unfold t_subst1; now rewrite <- 2 t_sub_sub, a_sub1_sub.
Qed.

The Actual Instance

We can now instanciate the generic OGS construction.

#[global] Instance ulc_val_laws : subst_monoid_laws val_m :=
  {| v_sub_proper := @m_sub_eq ;
     v_sub_var := @m_sub_id_r ;
     v_var_sub := @m_sub_id_l ;
     Subst.v_sub_sub := @m_sub_sub |} .

#[global] Instance ulc_conf_laws : subst_module_laws val_m state :=
  {| c_sub_proper := @s_sub_eq ;
     c_var_sub := @s_sub_id_l ;
     c_sub_sub := @s_sub_sub |} .


var_assumptions val_m

  
forall (Ξ“ : t_ctx) (x : ty),
injective (Subst.a_id (x:=x))
forall (Ξ“ : t_ctx) (x : ty) (v : val_m Ξ“ x),
decidable (is_var v)
forall (Ξ“1 Ξ“2 : t_ctx) (x : ty) (v : val_m Ξ“1 x)
  (r : Ξ“1 βŠ† Ξ“2), is_var (v_ren v r) -> is_var v

  
forall (Ξ“ : t_ctx) (x : ty),
injective (Subst.a_id (x:=x))
 intros ? [] ?? H; now dependent destruction H.
  
forall (Ξ“ : t_ctx) (x : ty) (v : val_m Ξ“ x),
decidable (is_var v)
 
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
decidable (is_var (Lam t))
Ξ“: t_ctx
t: term Ξ“
e: ev_ctx Ξ“
decidable (is_var (K1 t e))
Ξ“: t_ctx
v: val Ξ“
e: ev_ctx Ξ“
decidable (is_var (K2 v e))

    all: apply No; intro H; dependent destruction H.
  
forall (Ξ“1 Ξ“2 : t_ctx) (x : ty) (v : val_m Ξ“1 x)
  (r : Ξ“1 βŠ† Ξ“2), is_var (v_ren v r) -> is_var v
 intros ?? [] v r H; induction v; dependent destruction H; exact (Vvar _).
Qed.

#[global] Instance ulc_machine : machine val_m state obs_op :=
  {| eval := @ulc_eval ;
     oapp := @obs_app |} .

From Coinduction Require Import coinduction lattice rel tactics.
From OGS.ITree Require Import Eq.

Ltac refold_eval :=
  change (Structure.iter _ _ ?a) with (ulc_eval a);
  change (Structure.subst (fun pat : T1 => let 'T1_0 := pat in ?f) T1_0 ?u)
    with (bind_delay' u f).


machine_laws val_m state obs_op

  
Ξ“: t_ctx
x: ty
v: val_m Ξ“ x
o: obs x
Proper (asgn_eq (obs_dom o) Ξ“ ==> eq) (obs_app v o)
Ξ“1, Ξ“2: t_ctx
x: ty
v: val_m Ξ“1 x
o: obs x
a: obs_dom o =[ val_m ]> Ξ“1
b: Ξ“1 =[ val_m ]> Ξ“2
s_subst Ξ“1 (obs_app v o a) Ξ“2 b =
obs_app (m_subst Ξ“1 x v Ξ“2 b) o (a βŠ› b)
Ξ“, Ξ”: t_ctx
c: state Ξ“
a: Ξ“ =[ val_m ]> Ξ”
ulc_eval (s_subst Ξ“ c Ξ” a)
≋ bind_delay' (ulc_eval c)
    (fun n : Obs.nf obs_op val_m Ξ“ =>
     ulc_eval
       (s_subst Ξ“
          (obs_app (a_id (nf_ty n) (nf_var n))
             (nf_obs n) (nf_args n)) Ξ” a))
Ξ“: t_ctx
u: Obs.nf obs_op val_m Ξ“
ulc_eval
  (obs_app (a_id (nf_ty u) (nf_var u)) (nf_obs u)
     (nf_args u)) ≋ ret_delay u
well_founded head_inst_nostep

  
Ξ“: t_ctx
x: ty
v: val_m Ξ“ x
o: obs x
Proper (asgn_eq (obs_dom o) Ξ“ ==> eq) (obs_app v o)
 intros ?? H1; dependent elimination o; cbn; repeat (f_equal; auto).
  
Ξ“1, Ξ“2: t_ctx
x: ty
v: val_m Ξ“1 x
o: obs x
a: obs_dom o =[ val_m ]> Ξ“1
b: Ξ“1 =[ val_m ]> Ξ“2
s_subst Ξ“1 (obs_app v o a) Ξ“2 b =
obs_app (m_subst Ξ“1 x v Ξ“2 b) o (a βŠ› b)
 destruct x; dependent elimination o; cbn; f_equal.
  
Ξ“, Ξ”: t_ctx
c: state Ξ“
a: Ξ“ =[ val_m ]> Ξ”
ulc_eval (s_subst Ξ“ c Ξ” a)
≋ bind_delay' (ulc_eval c)
    (fun n : Obs.nf obs_op val_m Ξ“ =>
     ulc_eval
       (s_subst Ξ“
          (obs_app (a_id (nf_ty n) (nf_var n))
             (nf_obs n) (nf_args n)) Ξ” a))
 
Ξ“, Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
c: state Ξ“
e: Ξ“ =[ val_m ]> Ξ”
it_eq_bt Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
  (ulc_eval (s_subst Ξ“ c Ξ” e))
  (bind_delay' (ulc_eval c)
     (fun n : Obs.nf obs_op val_m Ξ“ =>
      ulc_eval
        (s_subst Ξ“
           (obs_app (a_id (nf_ty n) (nf_var n))
              (nf_obs n) (nf_args n)) Ξ” e)))

    
Ξ“: t_ctx
v: val Ξ“
i: Ξ“ βˆ‹ βŠ–
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: {| pr1 := ORet; pr2 := (! ▢ₐ v)%asgn |} =
{| pr1 := ORet; pr2 := (! ▢ₐ v)%asgn |}
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match e (βŠ–) i with
    | K0 c => inr (c β‹… ORet ⦇ ! ▢ₐ (v `α΅₯βŠ› e) ⦈)
    | K1 t e0 => inl (Cut t (K2 (v `α΅₯βŠ› e) e0))
    | K2 v0 e0 =>
        match v `α΅₯βŠ› e with
        | Var c =>
            fun (v1 : val Ξ”) (e1 : ev_ctx Ξ”) =>
            inr (c β‹… OApp ⦇ (! ▢ₐ v1) ▢ₐ e1 ⦈)
        | Lam t =>
            fun v1 : val Ξ” => inl ∘ Cut (t /[ v1])
        end v0 e0
    end
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match e (βŠ–) i with
    | K0 c => inr (c β‹… ORet ⦇ ! ▢ₐ (v `α΅₯βŠ› e) ⦈)
    | K1 t e0 => inl (Cut t (K2 (v `α΅₯βŠ› e) e0))
    | K2 v0 e0 =>
        match v `α΅₯βŠ› e with
        | Var c =>
            fun (v1 : val Ξ”) (e1 : ev_ctx Ξ”) =>
            inr (c β‹… OApp ⦇ (! ▢ₐ v1) ▢ₐ e1 ⦈)
        | Lam t =>
            fun v1 : val Ξ” => inl ∘ Cut (t /[ v1])
        end v0 e0
    end
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
Ξ“: t_ctx
v: val Ξ“
t: term Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut t (K2 v Ο€) = Cut t (K2 v Ο€)
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  (TauF
     (Structure.iter
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (state Ξ” ->
             itree Event.emptyβ‚‘
               ((fun _ : T1 => state Ξ”) +α΅’
                (fun _ : T1 => nf Ξ”)) x) in
          ret_delay ∘ eval_step) T1_0
        (Cut (t `β‚œβŠ› e) (K2 (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)))))
  (TauF
     (Structure.subst
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (Obs.nf obs_op val_m Ξ“ ->
             itree Event.emptyβ‚‘
               (fun _ : T1 => Obs.nf obs_op val_m Ξ”) x)
          in
          fun y : Obs.nf obs_op val_m Ξ“ =>
          ulc_eval
            (s_subst Ξ“
               (obs_app (a_id (nf_ty y) (nf_var y))
                  (nf_obs y) (nf_args y)) Ξ” e)) T1_0
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x := pat
             return
               (state Ξ“ ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ“) +α΅’
                   (fun _ : T1 => nf Ξ“)) x) in
             ret_delay ∘ eval_step) T1_0
           (Cut t (K2 v Ο€)))))
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ•
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: {| pr1 := OApp; pr2 := ((! ▢ₐ v) ▢ₐ Ο€)%asgn |} =
{| pr1 := OApp; pr2 := ((! ▢ₐ v) ▢ₐ Ο€)%asgn |}
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match e (βŠ•) i with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match e (βŠ•) i with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut (t /[ v]) Ο€ = Cut (t /[ v]) Ο€
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  (TauF
     (Structure.iter
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (state Ξ” ->
             itree Event.emptyβ‚‘
               ((fun _ : T1 => state Ξ”) +α΅’
                (fun _ : T1 => nf Ξ”)) x) in
          ret_delay ∘ eval_step) T1_0
        (Cut (t `β‚œβŠ› a_shift1 e /[ v `α΅₯βŠ› e]) (Ο€ `β‚‘βŠ› e))))
  (TauF
     (Structure.subst
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (Obs.nf obs_op val_m Ξ“ ->
             itree Event.emptyβ‚‘
               (fun _ : T1 => Obs.nf obs_op val_m Ξ”) x)
          in
          fun y : Obs.nf obs_op val_m Ξ“ =>
          ulc_eval
            (s_subst Ξ“
               (obs_app (a_id (nf_ty y) (nf_var y))
                  (nf_obs y) (nf_args y)) Ξ” e)) T1_0
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x := pat
             return
               (state Ξ“ ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ“) +α΅’
                   (fun _ : T1 => nf Ξ“)) x) in
             ret_delay ∘ eval_step) T1_0
           (Cut (t /[ v]) Ο€))))
Ξ“: t_ctx
t1, t2: term Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut t2 (K1 t1 Ο€) = Cut t2 (K1 t1 Ο€)
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  (TauF
     (Structure.iter
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (state Ξ” ->
             itree Event.emptyβ‚‘
               ((fun _ : T1 => state Ξ”) +α΅’
                (fun _ : T1 => nf Ξ”)) x) in
          ret_delay ∘ eval_step) T1_0
        (Cut (t2 `β‚œβŠ› e) (K1 (t1 `β‚œβŠ› e) (Ο€ `β‚‘βŠ› e)))))
  (TauF
     (Structure.subst
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (Obs.nf obs_op val_m Ξ“ ->
             itree Event.emptyβ‚‘
               (fun _ : T1 => Obs.nf obs_op val_m Ξ”) x)
          in
          fun y : Obs.nf obs_op val_m Ξ“ =>
          ulc_eval
            (s_subst Ξ“
               (obs_app (a_id (nf_ty y) (nf_var y))
                  (nf_obs y) (nf_args y)) Ξ” e)) T1_0
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x := pat
             return
               (state Ξ“ ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ“) +α΅’
                   (fun _ : T1 => nf Ξ“)) x) in
             ret_delay ∘ eval_step) T1_0
           (Cut t2 (K1 t1 Ο€)))))

    
Ξ“: t_ctx
v: val Ξ“
i: Ξ“ βˆ‹ βŠ–
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: {| pr1 := ORet; pr2 := (! ▢ₐ v)%asgn |} =
{| pr1 := ORet; pr2 := (! ▢ₐ v)%asgn |}
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match e (βŠ–) i with
    | K0 c => inr (c β‹… ORet ⦇ ! ▢ₐ (v `α΅₯βŠ› e) ⦈)
    | K1 t e0 => inl (Cut t (K2 (v `α΅₯βŠ› e) e0))
    | K2 v0 e0 =>
        match v `α΅₯βŠ› e with
        | Var c =>
            fun (v1 : val Ξ”) (e1 : ev_ctx Ξ”) =>
            inr (c β‹… OApp ⦇ (! ▢ₐ v1) ▢ₐ e1 ⦈)
        | Lam t =>
            fun v1 : val Ξ” => inl ∘ Cut (t /[ v1])
        end v0 e0
    end
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match e (βŠ–) i with
    | K0 c => inr (c β‹… ORet ⦇ ! ▢ₐ (v `α΅₯βŠ› e) ⦈)
    | K1 t e0 => inl (Cut t (K2 (v `α΅₯βŠ› e) e0))
    | K2 v0 e0 =>
        match v `α΅₯βŠ› e with
        | Var c =>
            fun (v1 : val Ξ”) (e1 : ev_ctx Ξ”) =>
            inr (c β‹… OApp ⦇ (! ▢ₐ v1) ▢ₐ e1 ⦈)
        | Lam t =>
            fun v1 : val Ξ” => inl ∘ Cut (t /[ v1])
        end v0 e0
    end
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
 
Ξ“: t_ctx
v: val Ξ“
i: Ξ“ βˆ‹ βŠ–
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: {| pr1 := ORet; pr2 := (! ▢ₐ v)%asgn |} =
{| pr1 := ORet; pr2 := (! ▢ₐ v)%asgn |}
v0: val Ξ”
v1: ev_ctx Ξ”
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match v `α΅₯βŠ› e with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end v0 v1
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match v `α΅₯βŠ› e with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end v0 v1
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end

      
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ–
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
v0: val Ξ”
v1: ev_ctx Ξ”
v': val Ξ”
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match v' with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end v0 v1
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match v' with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end v0 v1
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end

      dependent elimination v'; cbn; auto.
    
Ξ“: t_ctx
v: val Ξ“
t: term Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut t (K2 v Ο€) = Cut t (K2 v Ο€)
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  (TauF
     (Structure.iter
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (state Ξ” ->
             itree Event.emptyβ‚‘
               ((fun _ : T1 => state Ξ”) +α΅’
                (fun _ : T1 => nf Ξ”)) x) in
          ret_delay ∘ eval_step) T1_0
        (Cut (t `β‚œβŠ› e) (K2 (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)))))
  (TauF
     (Structure.subst
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (Obs.nf obs_op val_m Ξ“ ->
             itree Event.emptyβ‚‘
               (fun _ : T1 => Obs.nf obs_op val_m Ξ”) x)
          in
          fun y : Obs.nf obs_op val_m Ξ“ =>
          ulc_eval
            (s_subst Ξ“
               (obs_app (a_id (nf_ty y) (nf_var y))
                  (nf_obs y) (nf_args y)) Ξ” e)) T1_0
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x := pat
             return
               (state Ξ“ ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ“) +α΅’
                   (fun _ : T1 => nf Ξ“)) x) in
             ret_delay ∘ eval_step) T1_0
           (Cut t (K2 v Ο€)))))
 econstructor; refold_eval; apply CIH.
    
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ•
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: {| pr1 := OApp; pr2 := ((! ▢ₐ v) ▢ₐ Ο€)%asgn |} =
{| pr1 := OApp; pr2 := ((! ▢ₐ v) ▢ₐ Ο€)%asgn |}
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match e (βŠ•) i with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match e (βŠ•) i with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
 
Ξ“: t_ctx
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
vv: val_m Ξ” (βŠ•)
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  match
    match vv with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end
  match
    match vv with
    | Var c =>
        fun (v0 : val Ξ”) (e0 : ev_ctx Ξ”) =>
        inr (c β‹… OApp ⦇ (! ▢ₐ v0) ▢ₐ e0 ⦈)
    | Lam t => fun v0 : val Ξ” => inl ∘ Cut (t /[ v0])
    end (v `α΅₯βŠ› e) (Ο€ `β‚‘βŠ› e)
  with
  | inl x =>
      TauF
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x0 := pat
             return
               (state Ξ” ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ”) +α΅’
                   (fun _ : T1 => nf Ξ”)) x0) in
             ret_delay ∘ eval_step) T1_0 x)
  | inr y => RetF y
  end

      dependent elimination vv; cbn; auto.
    
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut (t /[ v]) Ο€ = Cut (t /[ v]) Ο€
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  (TauF
     (Structure.iter
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (state Ξ” ->
             itree Event.emptyβ‚‘
               ((fun _ : T1 => state Ξ”) +α΅’
                (fun _ : T1 => nf Ξ”)) x) in
          ret_delay ∘ eval_step) T1_0
        (Cut (t `β‚œβŠ› a_shift1 e /[ v `α΅₯βŠ› e]) (Ο€ `β‚‘βŠ› e))))
  (TauF
     (Structure.subst
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (Obs.nf obs_op val_m Ξ“ ->
             itree Event.emptyβ‚‘
               (fun _ : T1 => Obs.nf obs_op val_m Ξ”) x)
          in
          fun y : Obs.nf obs_op val_m Ξ“ =>
          ulc_eval
            (s_subst Ξ“
               (obs_app (a_id (nf_ty y) (nf_var y))
                  (nf_obs y) (nf_args y)) Ξ” e)) T1_0
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x := pat
             return
               (state Ξ“ ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ“) +α΅’
                   (fun _ : T1 => nf Ξ“)) x) in
             ret_delay ∘ eval_step) T1_0
           (Cut (t /[ v]) Ο€))))
 
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut (t /[ v]) Ο€ = Cut (t /[ v]) Ο€
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
  (ulc_eval
     (Cut
        (t `β‚œβŠ› a_shift1 e /[ (v : val_m Ξ“ (βŠ•)) α΅₯βŠ› e])
        (Ο€ `β‚‘βŠ› e)))
  (bind_delay' (ulc_eval (Cut (t /[ v]) Ο€))
     (fun y : Obs.nf obs_op val_m Ξ“ =>
      ulc_eval
        (s_subst Ξ“
           (obs_app (a_id (nf_ty y) (nf_var y))
              (nf_obs y) (nf_args y)) Ξ” e)))

      
Ξ“: t_ctx
t: term (Ξ“ β–Άβ‚“ βŠ•)
v: val Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut (t /[ v]) Ο€ = Cut (t /[ v]) Ο€
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
  (ulc_eval (Cut ((t /[ v]) `β‚œβŠ› e) (Ο€ `β‚‘βŠ› e)))
  (bind_delay' (ulc_eval (Cut (t /[ v]) Ο€))
     (fun y : Obs.nf obs_op val_m Ξ“ =>
      ulc_eval
        (s_subst Ξ“
           (obs_app (a_id (nf_ty y) (nf_var y))
              (nf_obs y) (nf_args y)) Ξ” e)))

      apply CIH.
    
Ξ“: t_ctx
t1, t2: term Ξ“
Ο€: ev_ctx Ξ“
Ξ”: t_ctx
R: relα΅’
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
  (itree Event.emptyβ‚‘
     (fun _ : T1 => Obs.nf obs_op val_m Ξ”))
CIH: forall (c : state Ξ“) (a : Ξ“ =[ val_m ]> Ξ”),
it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R T1_0
(ulc_eval (s_subst Ξ“ c Ξ” a))
(bind_delay' (ulc_eval c)
(fun n : Obs.nf obs_op val_m Ξ“ =>
ulc_eval
(s_subst Ξ“
(obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ” a)))
e: Ξ“ =[ val_m ]> Ξ”
H: Cut t2 (K1 t1 Ο€) = Cut t2 (K1 t1 Ο€)
it_eqF Event.emptyβ‚‘ (fun _ : T1 => nf_eq)
  (it_eq_t Event.emptyβ‚‘ (fun _ : T1 => nf_eq) R) T1_0
  (TauF
     (Structure.iter
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (state Ξ” ->
             itree Event.emptyβ‚‘
               ((fun _ : T1 => state Ξ”) +α΅’
                (fun _ : T1 => nf Ξ”)) x) in
          ret_delay ∘ eval_step) T1_0
        (Cut (t2 `β‚œβŠ› e) (K1 (t1 `β‚œβŠ› e) (Ο€ `β‚‘βŠ› e)))))
  (TauF
     (Structure.subst
        (fun pat : T1 =>
         let
         'T1_0 as x := pat
          return
            (Obs.nf obs_op val_m Ξ“ ->
             itree Event.emptyβ‚‘
               (fun _ : T1 => Obs.nf obs_op val_m Ξ”) x)
          in
          fun y : Obs.nf obs_op val_m Ξ“ =>
          ulc_eval
            (s_subst Ξ“
               (obs_app (a_id (nf_ty y) (nf_var y))
                  (nf_obs y) (nf_args y)) Ξ” e)) T1_0
        (Structure.iter
           (fun pat : T1 =>
            let
            'T1_0 as x := pat
             return
               (state Ξ“ ->
                itree Event.emptyβ‚‘
                  ((fun _ : T1 => state Ξ“) +α΅’
                   (fun _ : T1 => nf Ξ“)) x) in
             ret_delay ∘ eval_step) T1_0
           (Cut t2 (K1 t1 Ο€)))))
 econstructor; refold_eval; apply CIH.
  
Ξ“: t_ctx
u: Obs.nf obs_op val_m Ξ“
ulc_eval
  (obs_app (a_id (nf_ty u) (nf_var u)) (nf_obs u)
     (nf_args u)) ≋ ret_delay u
 
Ξ“: t_ctx
a: ty
i: Ξ“ βˆ‹ a
p: obs_op a
Ξ³: dom p =[ val_m ]> Ξ“
ulc_eval
  (obs_app (a_id a i) p (nf_args (i β‹… p ⦇ Ξ³ ⦈)))
≋ ret_delay (i β‹… p ⦇ Ξ³ ⦈)

    
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ–
Ξ³: dom ORet =[ val_m ]> Ξ“
ulc_eval (Cut (Val (Ξ³ (βŠ•) Ctx.top)) (K0 i))
≋ ret_delay (i β‹… ORet ⦇ Ξ³ ⦈)
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ•
Ξ³: dom OApp =[ val_m ]> Ξ“
ulc_eval
  (Cut (Val (Var i))
     (K2 (Ξ³ (βŠ•) (pop Ctx.top)) (Ξ³ (βŠ–) Ctx.top)))
≋ ret_delay (i β‹… OApp ⦇ Ξ³ ⦈)

    
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ–
Ξ³: dom ORet =[ val_m ]> Ξ“
nf_eq (i β‹… ORet ⦇ ! ▢ₐ Ξ³ (βŠ•) Ctx.top ⦈)
  (i β‹… ORet ⦇ Ξ³ ⦈)
Ξ“: t_ctx
i: Ξ“ βˆ‹ βŠ•
Ξ³: dom OApp =[ val_m ]> Ξ“
nf_eq
  (i
   β‹… OApp
     ⦇ (! ▢ₐ Ξ³ (βŠ•) (pop Ctx.top)) ▢ₐ Ξ³ (βŠ–) Ctx.top ⦈)
  (i β‹… OApp ⦇ Ξ³ ⦈)

    all: econstructor; intros ? v; do 3 (dependent elimination v; auto).
  
well_founded head_inst_nostep
 
x: ty
p: obs x
Acc head_inst_nostep (x,' p)

    
forall y : {x : ty & obs x},
head_inst_nostep y (βŠ•,' OApp) ->
Acc head_inst_nostep y
forall y : {x : ty & obs x},
head_inst_nostep y (βŠ–,' ORet) ->
Acc head_inst_nostep y

    
forall y : {x : ty & obs x},
head_inst_nostep y (βŠ•,' OApp) ->
Acc head_inst_nostep y
 
z: ty
p: obs z
H: head_inst_nostep (z,' p) (βŠ•,' OApp)
Acc head_inst_nostep (z,' p)

      
Ξ“: t_ctx
v: val_m Ξ“ (βŠ•)
a: dom OApp =[ val_m ]> Ξ“
i: Ξ“ βˆ‹ projT1 (βŠ–,' ORet)
t0: Β¬ (is_var v)
i0: evalβ‚’ (v βŠ™ OApp β¦— a ⦘)
β‰Š ret_delay (i β‹… projT2 (βŠ–,' ORet))
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
v: val_m Ξ“ (βŠ•)
a: dom OApp =[ val_m ]> Ξ“
i: Ξ“ βˆ‹ projT1 (βŠ•,' OApp)
t0: Β¬ (is_var v)
i0: evalβ‚’ (v βŠ™ OApp β¦— a ⦘)
β‰Š ret_delay (i β‹… projT2 (βŠ•,' OApp))
Acc head_inst_nostep (βŠ•,' OApp)

      
Ξ“: t_ctx
t1: term (Ξ“ β–Άβ‚“ βŠ•)
a: dom OApp =[ val_m ]> Ξ“
i: Ξ“ βˆ‹ projT1 (βŠ–,' ORet)
t0: Β¬ (is_var (Lam t1))
i0: evalβ‚’ (Lam t1 βŠ™ OApp β¦— a ⦘)
β‰Š ret_delay (i β‹… projT2 (βŠ–,' ORet))
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
t1: term (Ξ“ β–Άβ‚“ βŠ•)
a: dom OApp =[ val_m ]> Ξ“
i: Ξ“ βˆ‹ projT1 (βŠ•,' OApp)
t0: Β¬ (is_var (Lam t1))
i0: evalβ‚’ (Lam t1 βŠ™ OApp β¦— a ⦘)
β‰Š ret_delay (i β‹… projT2 (βŠ•,' OApp))
Acc head_inst_nostep (βŠ•,' OApp)

      all: apply it_eq_step in i0; now inversion i0.
    
forall y : {x : ty & obs x},
head_inst_nostep y (βŠ–,' ORet) ->
Acc head_inst_nostep y
 
z: ty
p: obs z
H: head_inst_nostep (z,' p) (βŠ–,' ORet)
Acc head_inst_nostep (z,' p)

      
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Acc head_inst_nostep (βŠ•,' OApp)

      
Ξ“: t_ctx
t1: term Ξ“
e: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var (K1 t1 e))
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) (K1 t1 e))
β‰Š ret_delay (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
v: val Ξ“
e0: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var (K2 v e0))
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) (K2 v e0))
β‰Š ret_delay (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Acc head_inst_nostep (βŠ•,' OApp)

      
Ξ“: t_ctx
t1: term Ξ“
e: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var (K1 t1 e))
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) (K1 t1 e))
β‰Š ret_delay (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)
 apply it_eq_step in i0; now inversion i0.
      
Ξ“: t_ctx
v: val Ξ“
e0: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var (K2 v e0))
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) (K2 v e0))
β‰Š ret_delay (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)
 
Ξ“: t_ctx
v: val Ξ“
e0: ev_ctx Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var (K2 v e0))
vv: val_m Ξ“ (βŠ•)
i0: evalβ‚’ (Cut (Val vv) (K2 v e0))
β‰Š ret_delay (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)

        
Ξ“: t_ctx
v: val Ξ“
e0: ev_ctx Ξ“
i: cvar Ξ“ (βŠ–)
t0: Β¬ (is_var (K2 v e0))
c: Ξ“ βˆ‹ βŠ•
r_rel: eqα΅’ (fun _ : T1 => obs_op βˆ™ Ξ“) T1_0
  (c β‹… OApp ⦇ (! ▢ₐ v) ▢ₐ e0 ⦈) 
  (i β‹… ORet)
Acc head_inst_nostep (βŠ–,' ORet)

        inversion r_rel.
      
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Acc head_inst_nostep (βŠ•,' OApp)
 
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
z: ty
p: obs z
H: head_inst_nostep (z,' p) (βŠ•,' OApp)
Acc head_inst_nostep (z,' p)

        
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Ξ“0: t_ctx
v0: val_m Ξ“0 (βŠ•)
a0: dom OApp =[ val_m ]> Ξ“0
i1: Ξ“0 βˆ‹ projT1 (βŠ–,' ORet)
t1: Β¬ (is_var v0)
i2: evalβ‚’ (v0 βŠ™ OApp β¦— a0 ⦘)
β‰Š ret_delay (i1 β‹… projT2 (βŠ–,' ORet))
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Ξ“0: t_ctx
v0: val_m Ξ“0 (βŠ•)
a0: dom OApp =[ val_m ]> Ξ“0
i1: Ξ“0 βˆ‹ projT1 (βŠ•,' OApp)
t1: Β¬ (is_var v0)
i2: evalβ‚’ (v0 βŠ™ OApp β¦— a0 ⦘)
β‰Š ret_delay (i1 β‹… projT2 (βŠ•,' OApp))
Acc head_inst_nostep (βŠ•,' OApp)

        
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Ξ“0: t_ctx
t2: term (Ξ“0 β–Άβ‚“ βŠ•)
a0: dom OApp =[ val_m ]> Ξ“0
i1: Ξ“0 βˆ‹ projT1 (βŠ–,' ORet)
t1: Β¬ (is_var (Lam t2))
i2: evalβ‚’ (Lam t2 βŠ™ OApp β¦— a0 ⦘)
β‰Š ret_delay (i1 β‹… projT2 (βŠ–,' ORet))
Acc head_inst_nostep (βŠ–,' ORet)
Ξ“: t_ctx
v: ev_ctx Ξ“
a: (βˆ…β‚“ β–Άβ‚“ βŠ•) =[ val_m ]> Ξ“
i: cvar Ξ“ (βŠ•)
t0: Β¬ (is_var v)
i0: evalβ‚’ (Cut (Val (a (βŠ•) Ctx.top)) v)
β‰Š ret_delay (i β‹… OApp)
Ξ“0: t_ctx
t2: term (Ξ“0 β–Άβ‚“ βŠ•)
a0: dom OApp =[ val_m ]> Ξ“0
i1: Ξ“0 βˆ‹ projT1 (βŠ•,' OApp)
t1: Β¬ (is_var (Lam t2))
i2: evalβ‚’ (Lam t2 βŠ™ OApp β¦— a0 ⦘)
β‰Š ret_delay (i1 β‹… projT2 (βŠ•,' OApp))
Acc head_inst_nostep (βŠ•,' OApp)

        all: apply it_eq_step in i2; now inversion i2.
Qed.

Concrete soundness theorem

Definition subst_eq Ξ” {Ξ“} : relation (state Ξ“) :=
  fun u v => forall Οƒ : Ξ“ =[val_m]> Ξ”, evalβ‚’ (u β‚œβŠ› Οƒ) β‰ˆ evalβ‚’ (v β‚œβŠ› Οƒ) .
Notation "x β‰ˆβŸ¦sub Ξ” βŸ§β‰ˆ y" := (subst_eq Ξ” x y) (at level 10).


Ξ”, Ξ“: t_ctx
x, y: state Ξ“
x β‰ˆβŸ¦ogs Ξ” βŸ§β‰ˆ y -> x β‰ˆβŸ¦sub Ξ” βŸ§β‰ˆ y

  exact (ogs_correction Ξ” x y).
Qed.

Recovering CIU-equivalence

Definition ciu_eq Ξ” {Ξ“} : relation (term Ξ“) :=
  fun u v => forall (Οƒ : Ξ“ =[val_m]> Ξ”) (Ο€ : ev_ctx Ξ”),
      evalβ‚’ (Cut (u `β‚œβŠ› Οƒ) Ο€) β‰ˆ evalβ‚’ (Cut (v `β‚œβŠ› Οƒ) Ο€) .
Notation "x β‰ˆβŸ¦ciu Ξ” βŸ§β‰ˆ y" := (ciu_eq Ξ” x y) (at level 10).

Definition c_init {Ξ“} (t : term Ξ“) : state (Ξ“ β–Άβ‚“ βŠ–)
  := Cut (t_shift1 t) (K0 Ctx.top) .

Definition a_of_sk {Ξ“ Ξ”} (Οƒ : Ξ“ =[val_m]> Ξ”) (Ο€ : ev_ctx Ξ”)
  : (Ξ“ β–Άβ‚“ βŠ–) =[val_m]> Ξ” := Οƒ ▢ₐ (Ο€ : val_m _ (βŠ–)) .


Ξ“, Ξ”: t_ctx
t: term Ξ“
Οƒ: Ξ“ =[ val_m ]> Ξ”
Ο€: ev_ctx Ξ”
Cut (t `β‚œβŠ› Οƒ) Ο€ = c_init t β‚œβŠ› a_of_sk Οƒ Ο€

  cbn; unfold t_shift1; now rewrite t_sub_ren.
Qed.

We can now obtain a correctness theorem with respect to standard CIU-equivalence by embedding terms into states. Proving that CIU-equivalence entails our substitution equivalence is left to the reader!

Ξ”, Ξ“: t_ctx
x, y: term Ξ“
c_init x β‰ˆβŸ¦ogs Ξ” βŸ§β‰ˆ c_init y -> x β‰ˆβŸ¦ciu Ξ” βŸ§β‰ˆ y

  
Ξ”, Ξ“: t_ctx
x, y: term Ξ“
H: c_init x β‰ˆβŸ¦ogs Ξ” βŸ§β‰ˆ c_init y
Οƒ: Ξ“ =[ val_m ]> Ξ”
k: ev_ctx Ξ”
evalβ‚’ (c_init x β‚œβŠ› a_of_sk Οƒ k)
β‰ˆ evalβ‚’ (c_init y β‚œβŠ› a_of_sk Οƒ k)

  now apply ulc_subst_correct.
Qed.

Example terms

Following a trick by Conor McBride we provide a cool notation for writing terms without any DeBruijn indices, instead leveraging Coq's binders. For this we need a bit of infrastructure, for manipulating terms that only have term variables.

Equations n_ctx : nat -> t_ctx :=
  n_ctx O     := βˆ… ;
  n_ctx (S n) := n_ctx n β–Άβ‚“ βŠ• .

Notation var' n := (n_ctx n βˆ‹ βŠ•).
Notation term' n := (term (n_ctx n)).

Equations v_emb (n : nat) : var' (S n) :=
  v_emb O     := Ctx.top ;
  v_emb (S n) := pop (v_emb n) .

Equations v_lift {n} : var' n -> var' (S n) :=
  @v_lift (S _) Ctx.top     := Ctx.top ;
  @v_lift (S _) (pop i) := pop (v_lift i) .

Here starts the magic.

Equations mk_var (m : nat) : forall n, var' (m + S n) :=
  mk_var O     := v_emb ;
  mk_var (S m) := v_lift ∘ mk_var m .

Definition mk_lam {m : nat} (f : (forall n, term' (m + S n)) -> term' (S m)) : term' m
  := Val (Lam (f (Val ∘ Var ∘ mk_var m))).
Arguments mk_lam {_} & _ .

Now a bit of syntactic sugar.

Declare Custom Entry lambda.
Notation "✨ e ✨" := (e : term' 0) (e custom lambda at level 2).
Notation "x" := (x _) (in custom lambda at level 0, x ident).
Notation "( x )" := x (in custom lambda at level 0, x at level 2).
Notation "x y" := (App x y)
  (in custom lambda at level 1, left associativity).
Notation "'Ξ»' x .. y β‡’ U" :=
  (mk_lam (fun x => .. (mk_lam (fun y => U)) ..))
  (in custom lambda at level 1, x binder, y binder, U at level 2).

Aren't these beautiful?

Definition Delta := ✨ (Ξ» x β‡’ x x) ✨ .
Definition Omega := ✨ (Ξ» x β‡’ x x) (Ξ» x β‡’ x x) ✨ .
Definition Upsilon := ✨ Ξ» f β‡’ (Ξ» x β‡’ f (x x)) (Ξ» x β‡’ f (x x)) ✨.
Definition Theta := ✨ (Ξ» x f β‡’ f (x x f)) (Ξ» x f β‡’ f (x x f)) ✨.

You can check the actual lambda-term they unwrap to by running eg:

= Val
    (Lam
       (App
          (Val
             (Lam
                (App (Val (Var (pop Ctx.top)))
                   (App (Val (Var Ctx.top))
                      (Val (Var Ctx.top))))))
          (Val
             (Lam
                (App (Val (Var (pop Ctx.top)))
                   (App (Val (Var Ctx.top))
                      (Val (Var Ctx.top))))))))
: term' 0