From 554c00266a8846d30be21ecc761aa9e6b9f88cb8 Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Mon, 17 Mar 2025 01:00:47 +0100
Subject: [PATCH 1/2] Add TApp

---
 PLC.v       | 174 +++++++++++++++++++++++++++++++++++++---------------
 _CoqProject |   1 +
 2 files changed, 125 insertions(+), 50 deletions(-)

diff --git a/PLC.v b/PLC.v
index 14f2a15..d502514 100644
--- a/PLC.v
+++ b/PLC.v
@@ -30,7 +30,7 @@ Import ListNotations.
 
 (** ** Bijections *)
 
-Record iso (A B : Type) : Type :=
+Record iso (A B : Set) : Set :=
   { iso_from : A -> B
   ; iso_to   : B -> A
   }.
@@ -73,7 +73,7 @@ Definition iso_eq {A A'}
 (** ** Generic collections *)
 
 (** Bounded nats *)
-Fixpoint bnat (n : nat) : Type :=
+Fixpoint bnat (n : nat) : Set :=
   match n with
   | O => Empty_set
   | S n => option (bnat n)
@@ -135,7 +135,7 @@ Fixpoint lookup_list {A : Type} (xs : list A) : bnat (length xs) -> A :=
     end
   end.
 
-Fixpoint lookup_hlist {A} {f : A -> Type} {vs : list A}
+Fixpoint lookup_hlist {A : Type} {f : A -> Type} {vs : list A}
   : forall v : bnat (length vs), hlist f vs -> f (lookup_list vs v) :=
   match vs with
   | [] => fun v => match v with end
@@ -146,7 +146,7 @@ Fixpoint lookup_hlist {A} {f : A -> Type} {vs : list A}
     end
   end.
 
-Fixpoint lookup_ziphlist {A B} {f : A -> B -> Type} {n : nat}
+Fixpoint lookup_ziphlist {A B : Type} {f : A -> B -> Type} {n : nat}
   : forall {ts1 : lilist A n} {ts2 : lilist B n} (tv : bnat n),
       ziphlist f ts1 ts2 -> f (lookup_lilist tv ts1) (lookup_lilist tv ts2) :=
   match n with
@@ -158,8 +158,8 @@ Fixpoint lookup_ziphlist {A B} {f : A -> B -> Type} {n : nat}
       end
   end.
 
-Definition rel_list {n : nat} : lilist Type n -> lilist Type n -> Type :=
-  ziphlist (fun a b => a -> b -> Prop).
+Definition rel_list {n : nat} : lilist Set n -> lilist Set n -> Type :=
+  ziphlist (fun a b : Set => a -> b -> Prop).
 
 (** *** Insertion *)
 
@@ -180,7 +180,7 @@ Fixpoint insert_bnat (m : nat) {n : nat} : bnat n -> bnat (S n) :=
   end.
 
 (** Insert an element at position [n]. *)
-Fixpoint insert_lilist {A} (m : nat) (t0 : A) {n : nat}
+Fixpoint insert_lilist {A : Type} (m : nat) (t0 : A) {n : nat}
   : lilist A n -> lilist A (S n) :=
   match m with
   | O => fun ts => (t0, ts)
@@ -191,8 +191,8 @@ Fixpoint insert_lilist {A} (m : nat) (t0 : A) {n : nat}
     end
   end.
 
-Fixpoint eq_insert_lookup_lilist (m : nat) (t0 : Type) {n : nat}
-  : forall {ts : lilist Type n} (tv : bnat n),
+Fixpoint eq_insert_lookup_lilist (m : nat) (t0 : Set) {n : nat}
+  : forall {ts : lilist Set n} (tv : bnat n),
         lookup_lilist tv ts
       = lookup_lilist (insert_bnat m tv) (insert_lilist m t0 ts) :=
   match n with
@@ -208,14 +208,14 @@ Fixpoint eq_insert_lookup_lilist (m : nat) (t0 : Type) {n : nat}
     end
   end.
 
-Definition iso_insert_lookup_lilist (m : nat) (t0 : Type) {n : nat}
-  : forall {ts : lilist Type n} (tv : bnat n),
+Definition iso_insert_lookup_lilist (m : nat) (t0 : Set) {n : nat}
+  : forall {ts : lilist Set n} (tv : bnat n),
       iso (lookup_lilist tv ts) (lookup_lilist (insert_bnat m tv) (insert_lilist m t0 ts)) :=
   fun ts tv => iso_eq (eq_insert_lookup_lilist m t0 tv).
 
 Fixpoint insert_lookup_rel_list (m : nat) {n : nat}
-  {t01 t02 : Type} (r0 : t01 -> t02 -> Prop)
-  : forall {ts01 ts02 : lilist Type n},
+  {t01 t02 : Set} (r0 : t01 -> t02 -> Prop)
+  : forall {ts01 ts02 : lilist Set n},
       rel_list ts01 ts02 -> rel_list (insert_lilist m t01 ts01) (insert_lilist m t02 ts02) :=
   match m with
   | O => fun _ _ rs => (r0, rs)
@@ -242,7 +242,7 @@ t ::= t -> t     (* Function *)
     | t + t      (* Sum *)
 >>
   *)
-Inductive ty (n : nat) : Type :=
+Inductive ty (n : nat) : Set :=
 | Arrow : ty n -> ty n -> ty n
 | Forall : ty (S n) -> ty n
 | Tyvar : bnat n -> ty n
@@ -284,6 +284,32 @@ Fixpoint shift_ty (m : nat) {n : nat} (t : ty n) : ty (S n) :=
   | Sum t1 t2 => Sum (shift_ty m t1) (shift_ty m t2)
   end.
 
+Fixpoint match_tyvar (m : nat) {n : nat} (v : bnat (S n)) : option (bnat n) :=
+  match m, n, v with
+  | O, _, None => None
+  | O, _, Some v => Some v
+  | S m, O, _ => None (* should not happen *)
+  | S m, S n, None => Some None
+  | S m, S n, Some v => match match_tyvar m v with
+    | None => None
+    | Some w => Some (Some w)
+    end
+  end.
+
+(* t[u/m] *)
+Fixpoint sub_ty (m : nat) {n : nat} (u : ty n) (t : ty (S n)) : ty n :=
+  match t with
+  | Arrow t1 t2 => Arrow (sub_ty m u t1) (sub_ty m u t2)
+  | Forall t => Forall (sub_ty (S m) (shift_ty 0 u) t)
+  | Tyvar v => match match_tyvar m v with
+    | None => u
+    | Some v => Tyvar v
+    end
+  | Unit => Unit
+  | Prod t1 t2 => Prod (sub_ty m u t1) (sub_ty m u t2)
+  | Sum t1 t2 => Sum (sub_ty m u t1) (sub_ty m u t2)
+  end.
+
 (** *** Terms *)
 
 Section Constants.
@@ -291,7 +317,7 @@ Section Constants.
 Context {n : nat}.
 
 (** Constants *)
-Inductive cn : ty n -> Type :=
+Inductive cn : ty n -> Set :=
 | One : cn Unit
   (* [unit] *)
 
@@ -328,10 +354,14 @@ u ::= tyfun u   (* Type abstraction *)
     | c         (* Constant *)
 >>
   *)
-Inductive tm (n : nat) (vs : list (ty n)) : ty n -> Type :=
+Inductive tm (n : nat) (vs : list (ty n)) : ty n -> Set :=
 | TAbs {t}
   : tm (S n) (map (shift_ty 0) vs) t ->
     tm n vs (Forall t)
+| TApp {t}
+  : tm n vs (Forall t) ->
+    forall (u : ty n),
+    tm n vs (sub_ty 0 u t)
 | Abs {t1 t2}
   : tm n (t1 :: vs) t2 ->
     tm n vs (Arrow t1 t2)
@@ -346,11 +376,12 @@ Inductive tm (n : nat) (vs : list (ty n)) : ty n -> Type :=
     tm n vs t
 .
 
-Arguments TAbs {n vs t}.
-Arguments Abs  {n vs t1 t2}.
-Arguments App  {n vs t1 t2}.
+Arguments TAbs {n vs t} &.
+Arguments TApp {n vs t}.
+Arguments Abs  {n vs t1 t2} &.
+Arguments App  {n vs t1 t2} &.
 Arguments Var  {n vs}.
-Arguments Con  {n vs t}.
+Arguments Con  {n vs t} &.
 
 Delimit Scope tm_scope with tm.
 Bind Scope tm_scope with tm.
@@ -365,11 +396,11 @@ Notation tm0 := (tm 0 []).
 (** *** Types *)
 
 (** Semantics of types as Coq types *)
-Fixpoint eval_ty {n : nat} (ts : lilist Type n) (t : ty n)
-  : Type :=
+Fixpoint eval_ty {n : nat} (ts : lilist Set n) (t : ty n)
+  : Set :=
   match t with
   | Arrow t1 t2 => eval_ty ts t1 -> eval_ty ts t2
-  | Forall t => forall (t0 : Type), @eval_ty (S n) (t0, ts) t
+  | Forall t => forall (t0 : Set), @eval_ty (S n) (t0, ts) t
   | Tyvar tv => lookup_lilist tv ts
   | Unit => unit
   | Prod t1 t2 => eval_ty ts t1 * eval_ty ts t2
@@ -377,7 +408,7 @@ Fixpoint eval_ty {n : nat} (ts : lilist Type n) (t : ty n)
   end.
 
 (** Semantics of types in the empty context. *)
-Definition eval_ty0 : ty 0 -> Type := @eval_ty 0 tt.
+Definition eval_ty0 : ty 0 -> Set := @eval_ty 0 tt.
 
 (** *** Terms *)
 
@@ -386,7 +417,7 @@ Definition eval_ty0 : ty 0 -> Type := @eval_ty 0 tt.
   variable denotes. *)
 
 (** Add a new variable-[Type] binding to the context of a term *)
-Fixpoint shift_eval (m : nat) {n : nat} {ts : lilist Type n} (t0 : Type) (t : ty n)
+Fixpoint shift_eval (m : nat) {n : nat} {ts : lilist Set n} (t0 : Set) (t : ty n)
   : iso (eval_ty ts t) (@eval_ty (S n) (insert_lilist m t0 ts) (shift_ty m t)) :=
   match t with
   | Arrow t1 t2 =>
@@ -396,13 +427,13 @@ Fixpoint shift_eval (m : nat) {n : nat} {ts : lilist Type n} (t0 : Type) (t : ty
        ; iso_to := fun f x0 => iso_to i2 (f (iso_from i1 x0))
       |}
   | Forall t =>
-      {| iso_from := fun (f : forall a : Type, @eval_ty (S n) (a, ts) t) a =>
+      {| iso_from := fun (f : forall a : Set, @eval_ty (S n) (a, ts) t) a =>
            let i := @shift_eval (S m) (S n) (a, ts) t0 t in
            iso_from i (f a)
-       ; iso_to := fun (f : forall a : Type, @eval_ty (S (S n)) (a, _) (shift_ty (S m) t)) a =>
+       ; iso_to := fun (f : forall a : Set, @eval_ty (S (S n)) (a, _) (shift_ty (S m) t)) a =>
            let i := @shift_eval (S m) (S n) (a, _) t0 t in
            iso_to i (f a)
-      |} : iso (forall (a : Type), @eval_ty (S n) (a, ts) t) _
+      |} : iso (forall (a : Set), @eval_ty (S n) (a, ts) t) _
   | Tyvar tv => iso_insert_lookup_lilist m t0 tv
   | Unit => iso_id
   | Prod t1 t2 => iso_prod (shift_eval m t0 t1) (shift_eval m t0 t2)
@@ -410,7 +441,7 @@ Fixpoint shift_eval (m : nat) {n : nat} {ts : lilist Type n} (t0 : Type) (t : ty
   end.
 
 (** Add a new variable-[Type] binding to the context of a context. *)
-Fixpoint shift_hlist {n : nat} {ts : lilist Type n} {vs : list (ty n)} (t0 : Type)
+Fixpoint shift_hlist {n : nat} {ts : lilist Set n} {vs : list (ty n)} (t0 : Set)
   : hlist (eval_ty ts) vs -> hlist (@eval_ty (S n) (t0, ts)) (map (shift_ty 0) vs) :=
   match vs with
   | [] => fun _ => tt
@@ -419,7 +450,7 @@ Fixpoint shift_hlist {n : nat} {ts : lilist Type n} {vs : list (ty n)} (t0 : Typ
   end.
 
 (** Semantics of constants as Coq values *)
-Definition eval_cn {n : nat} (ts : lilist Type n) {t : ty n} (c : cn t)
+Definition eval_cn {n : nat} (ts : lilist Set n) {t : ty n} (c : cn t)
   : eval_ty ts t :=
   match c with
   | One => tt
@@ -435,14 +466,34 @@ Definition eval_cn {n : nat} (ts : lilist Type n) {t : ty n} (c : cn t)
     end
   end.
 
+Lemma eval_ty_sub_ty (m : nat) {n : nat} (ts : lilist Set n) (u : ty n) (t : ty (S n))
+  : eval_ty ts (sub_ty m u t) = eval_ty (n := S n) (insert_lilist m (eval_ty ts u) ts) t.
+Proof.
+  revert n t m ts u. fix self 2. intros n t m ts u. destruct t; simpl.
+  - apply (f_equal2 (fun x y : Set => x -> y)); auto.
+  - 
+Admitted.
+
+Lemma eval_ty_sub_ty_0 {n : nat} (ts : lilist Set n) (u : ty n) (t : ty (S n))
+  : eval_ty ts (sub_ty 0 u t) = eval_ty (n := S n) (eval_ty ts u, ts) t.
+Proof.
+Admitted.
+
+Definition coerce_eval_sub {n : nat} (ts : lilist Set n) (u : ty n) (t : ty (S n))
+  : eval_ty (n := S n) (eval_ty ts u, ts) t -> eval_ty ts (sub_ty 0 u t) :=
+  match eval_ty_sub_ty_0 ts u t with
+  | eq_refl => fun x => x
+  end.
+
 (** Semantics of terms as Coq values *)
 Fixpoint eval_tm
-  {n : nat} (ts : lilist Type n)
+  {n : nat} (ts : lilist Set n)
   {vs : list (ty n)} (vls : hlist (eval_ty ts) vs)
   {t : ty n} (u : tm n vs t)
   : eval_ty ts t :=
-  match u with
-  | TAbs u => fun t0 => @eval_tm (S n) (t0, ts) _ (shift_hlist t0 vls) _ u
+  match u in tm _ _ t return eval_ty ts t with
+  | TAbs u => fun (t0 : Set) => @eval_tm (S n) (t0, ts) _ (shift_hlist t0 vls) _ u
+  | TApp u t => coerce_eval_sub ts t _ (eval_tm ts vls u (eval_ty ts t))
   | Abs u => fun x => @eval_tm _ ts (_ :: vs) (x, vls) _ u
   | App u1 u2 => (eval_tm ts vls u1) (eval_tm ts vls u2)
   | Var v => lookup_hlist v vls
@@ -457,15 +508,15 @@ Definition eval_tm0 {t : ty 0} : tm0 t -> eval_ty0 t :=
 
 (** Relational semantics of types *)
 Fixpoint eval2_ty {n : nat}
-  {ts1 ts2 : lilist Type n}
+  {ts1 ts2 : lilist Set n}
   (rs : rel_list ts1 ts2)
   (t : ty n)
   : eval_ty ts1 t -> eval_ty ts2 t -> Prop :=
-  match t with
-  | Arrow t1 t2 => fun f1 f2 =>
+  match t return eval_ty ts1 t -> eval_ty ts2 t -> Prop with
+  | Arrow t1 t2 => fun (f1 : eval_ty ts1 t1 -> eval_ty ts1 t2) f2 =>
       forall x1 x2, eval2_ty rs t1 x1 x2 -> eval2_ty rs t2 (f1 x1) (f2 x2)
   | Forall t => fun f1 f2 =>
-      forall (t01 t02 : Type) (r0 : t01 -> t02 -> Prop),
+      forall (t01 t02 : Set) (r0 : t01 -> t02 -> Prop),
         @eval2_ty (S n) (t01, ts1) (t02, ts2) (r0, rs) t (f1 t01) (f2 t02)
   | Tyvar tv => lookup_ziphlist tv rs
 
@@ -488,7 +539,7 @@ Definition eval2_ty0 (t : ty 0) : eval_ty0 t -> eval_ty0 t -> Prop :=
 (** Relational semantics of contexts *)
 Fixpoint eval2_ctx {n : nat} {vs : list (ty n)}
   : forall
-      {ts1 ts2 : lilist Type n} (rs : rel_list ts1 ts2)
+      {ts1 ts2 : lilist Set n} (rs : rel_list ts1 ts2)
       (vls1 : hlist (eval_ty ts1) vs) (vls2 : hlist (eval_ty ts2) vs),
         Prop :=
   match vs with
@@ -503,10 +554,10 @@ Fixpoint eval2_ctx {n : nat} {vs : list (ty n)}
 (* TODO: generalize *)
 Lemma param_insert_bnat_from (m : nat)
   : forall {n : nat}
-      (ts1 ts2 : lilist Type n)
+      (ts1 ts2 : lilist Set n)
       (rs : rel_list ts1 ts2)
       (v : bnat n)
-      (t01 t02 : Type) (r0 : t01 -> t02 -> Prop)
+      (t01 t02 : Set) (r0 : t01 -> t02 -> Prop)
       (vl1 : lookup_lilist v ts1) (vl2 : lookup_lilist v ts2)
       , lookup_ziphlist v rs vl1 vl2 ->
         lookup_ziphlist (insert_bnat m v) (insert_lookup_rel_list m r0 rs)
@@ -520,10 +571,10 @@ Qed.
 
 Lemma param_insert_bnat_to (m : nat)
   : forall {n : nat}
-      (ts1 ts2 : lilist Type n)
+      (ts1 ts2 : lilist Set n)
       (rs : rel_list ts1 ts2)
       (v : bnat n)
-      (t01 t02 : Type) (r0 : t01 -> t02 -> Prop)
+      (t01 t02 : Set) (r0 : t01 -> t02 -> Prop)
       (vl1' : lookup_lilist (insert_bnat m v) (insert_lilist m t01 ts1))
       (vl2' : lookup_lilist (insert_bnat m v) (insert_lilist m t02 ts2))
       , lookup_ziphlist (insert_bnat m v) (insert_lookup_rel_list m r0 rs) vl1' vl2'->
@@ -542,10 +593,10 @@ Arguments lookup_ziphlist : simpl never.
 Arguments lookup_lilist : simpl never.
 
 Lemma param_shift (m : nat) {n : nat}
-  (ts1 ts2 : lilist Type n)
+  (ts1 ts2 : lilist Set n)
   (rs : rel_list ts1 ts2)
   (t : ty n)
-  (t01 t02 : Type)
+  (t01 t02 : Set)
   (r0 : t01 -> t02 -> Prop)
   : (forall (vl1 : eval_ty ts1 t) (vl2 : eval_ty ts2 t),
        eval2_ty rs t vl1 vl2 ->
@@ -575,10 +626,10 @@ Qed.
 End Hack_param_shift.
 
 Lemma param_tabs {n : nat}
-  (ts1 ts2 : lilist Type n)
+  (ts1 ts2 : lilist Set n)
   (rs : rel_list ts1 ts2)
   (vs : list (ty n)) (vls1 : hlist (eval_ty ts1) vs) (vls2 : hlist (eval_ty ts2) vs)
-  (t01 t02 : Type)
+  (t01 t02 : Set)
   (r0 : t01 -> t02 -> Prop)
   : eval2_ctx rs vls1 vls2 ->
     @eval2_ctx (S n) _ (t01, ts1) (t02, ts2) (r0, rs)
@@ -591,8 +642,21 @@ Proof.
   apply (param_shift 0); auto.
 Qed.
 
+About coerce_eval_sub.
+About eval2_ty.
+
+Lemma param_tapp {n : nat}
+  (ts1 ts2 : lilist Set n)
+  (rs : rel_list ts1 ts2)
+  (u : ty n) (t : ty (S n))
+  (w1 : eval_ty (n := S n) (eval_ty ts1 u, ts1) t) (w2 : eval_ty (n := S n) (eval_ty ts2 u, ts2) t)
+  : eval2_ty (n := S n) (ts1 := (_, _)) (ts2 := (_, _)) (eval2_ty rs _, rs) _ w1 w2 ->
+    eval2_ty rs _ (coerce_eval_sub ts1 u t w1) (coerce_eval_sub ts2 u t w2).
+Proof.
+Admitted.
+
 Lemma param_var {n : nat}
-  (ts1 ts2 : lilist Type n)
+  (ts1 ts2 : lilist Set n)
   (rs : rel_list ts1 ts2)
   (vs : list (ty n)) (vls1 : hlist (eval_ty ts1) vs) (vls2 : hlist (eval_ty ts2) vs)
   (v : bnat (length vs))
@@ -604,7 +668,7 @@ Proof.
 Qed.
 
 Lemma param_cn {n : nat}
-  (ts1 ts2 : lilist Type n)
+  (ts1 ts2 : lilist Set n)
   (rs : rel_list ts1 ts2)
   (t : ty n)
   (c : cn t)
@@ -618,7 +682,7 @@ Qed.
 
 (** Main theorem! Every term satisfies the logical relation of its type. *)
 Theorem parametricity (n : nat)
-  (ts1 ts2 : lilist Type n)
+  (ts1 ts2 : lilist Set n)
   (rs : rel_list ts1 ts2)
   (vs : list (ty n)) (vls1 : hlist (eval_ty ts1) vs) (vls2 : hlist (eval_ty ts2) vs)
   (t : ty n)
@@ -629,6 +693,10 @@ Proof.
   - (* TAbs u *)
     auto using param_tabs.
 
+  - (* TApp u t *)
+    apply param_tapp.
+    apply IHu. auto.
+
   - (* Abs u *)
     apply IHu; split; auto.
 
@@ -664,9 +732,15 @@ Compute (eval2_ty0 ID_ty).
     identity function. Let [f] be the interpretation of [u] ([f := eval_tm0 u]),
     then [f _ a = a].
   *)
-Example parametric_ID (t : tm0 ID_ty) (A : Type) (a : A)
+Example parametric_ID (t : tm0 ID_ty) (A : Set) (a : A)
   : (eval_tm0 t) A a = a.
 Proof.
   pose proof (parametricity0 ID_ty t A A (fun x1 x2 => x1 = a) a a) as H.
   simpl in H; auto.
 Qed.
+
+Definition id : tm0 ID_ty :=
+  TAbs (Abs (Var (vs := _ :: []) V0)).
+
+Definition idid : tm0 ID_ty :=
+  App (TApp id _) id.
diff --git a/_CoqProject b/_CoqProject
index ed532a4..06f77a3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,2 +1,3 @@
 -Q ./ PLC
 ./PLC.v
+-arg -impredicative-set

From 514daba6e308578586d6f20f7cbc1c89ba96ff0f Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Mon, 17 Mar 2025 10:58:38 +0100
Subject: [PATCH 2/2] use iso

---
 PLC.v | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 63 insertions(+), 9 deletions(-)

diff --git a/PLC.v b/PLC.v
index d502514..0db355c 100644
--- a/PLC.v
+++ b/PLC.v
@@ -63,6 +63,29 @@ Definition iso_sum {A A' B B'}
          end
     |}.
 
+Definition iso_fun {A A' B B'}
+  : iso A A' -> iso B B' -> iso (A -> B) (A' -> B') :=
+  fun ia ib =>
+    {| iso_from := fun f => fun x => iso_from ib (f (iso_to ia x))
+     ; iso_to := fun f => fun x => iso_to ib (f (iso_from ia x))
+    |}.
+
+Definition iso_forall {A : Type} {B B' : A -> Set}
+  : (forall a, iso (B a) (B' a)) -> iso (forall a, B a) (forall a, B' a) :=
+  fun ib =>
+    {| iso_from := fun f => fun x => iso_from (ib x) (f x)
+     ; iso_to := fun f => fun x => iso_to (ib x) (f x)
+    |}.
+
+Definition iso_trans {A B C : Set}
+  : iso A B -> iso B C -> iso A C :=
+  fun ab bc =>
+    {| iso_from := fun x => iso_from bc (iso_from ab x)
+     ; iso_to := fun x => iso_to ab (iso_to bc x)
+    |}.
+
+(** *** Properties *)
+
 Definition iso_eq {A A'}
   : A = A' -> iso A A' :=
   fun e =>
@@ -466,24 +489,55 @@ Definition eval_cn {n : nat} (ts : lilist Set n) {t : ty n} (c : cn t)
     end
   end.
 
-Lemma eval_ty_sub_ty (m : nat) {n : nat} (ts : lilist Set n) (u : ty n) (t : ty (S n))
-  : eval_ty ts (sub_ty m u t) = eval_ty (n := S n) (insert_lilist m (eval_ty ts u) ts) t.
+Lemma eval_ty_shift_ty (m : nat) {n : nat} (A : Set) (ts : lilist Set n) (t : ty n)
+  : iso (eval_ty (insert_lilist m A ts) (shift_ty m t)) (eval_ty ts t).
 Proof.
-  revert n t m ts u. fix self 2. intros n t m ts u. destruct t; simpl.
-  - apply (f_equal2 (fun x y : Set => x -> y)); auto.
-  - 
+Admitted.
+
+Lemma eval_ty_sub_tyvar (m : nat) {n : nat} (ts : lilist Set n) (us : lilist Set (S n)) (u : ty n) (v : bnat (S n))
+  : ziphlist iso (insert_lilist m (eval_ty ts u) ts) us ->
+    iso (eval_ty ts (match match_tyvar m v with Some v => v | None => u end)) (lookup_lilist v us).
+Proof.
+  revert m n ts us u v. fix self 1. intros m n ts us u v Hts.
+  destruct m, v; simpl.
+  - admit.
+  - admit.
+  - destruct n; simpl.
+    { destruct b. }
+    { replace (match match match_tyvar m b with Some w => Some (Some w) | None => None end with Some v => Tyvar (n := S n) v | None => u end) with (match match_tyvar m b with Some w => Tyvar (n := S n) (Some w) | None => u end).
+      { admit. }
+      { destruct match_tyvar; reflexivity. }
+    }
+  - destruct n; simpl.
+    { admit. }
+    { admit. }
+Admitted.
+
+Lemma eval_ty_sub_ty (m : nat) {n : nat} (ts : lilist Set n) (us : lilist Set (S n)) (u : ty n) (t : ty (S n))
+  : ziphlist iso (insert_lilist m (eval_ty ts u) ts) us ->
+    iso (eval_ty ts (sub_ty m u t)) (eval_ty (n := S n) us t).
+Proof.
+  revert n t m ts us u. fix self 2. intros n t m ts us u Hts. destruct t; simpl.
+  - apply iso_fun; auto.
+  - apply iso_forall; intros.
+    apply self.
+    constructor; [ apply iso_id | ].
+    simpl snd.
+    admit.
+  - apply eval_ty_sub_tyvar. auto.
+  - apply iso_id.
+  - apply iso_prod; auto.
+  - apply iso_sum; auto.
 Admitted.
 
 Lemma eval_ty_sub_ty_0 {n : nat} (ts : lilist Set n) (u : ty n) (t : ty (S n))
-  : eval_ty ts (sub_ty 0 u t) = eval_ty (n := S n) (eval_ty ts u, ts) t.
+  : iso (eval_ty ts (sub_ty 0 u t)) (eval_ty (n := S n) (eval_ty ts u, ts) t).
 Proof.
 Admitted.
 
 Definition coerce_eval_sub {n : nat} (ts : lilist Set n) (u : ty n) (t : ty (S n))
   : eval_ty (n := S n) (eval_ty ts u, ts) t -> eval_ty ts (sub_ty 0 u t) :=
-  match eval_ty_sub_ty_0 ts u t with
-  | eq_refl => fun x => x
-  end.
+  iso_to (eval_ty_sub_ty_0 ts u t).
 
 (** Semantics of terms as Coq values *)
 Fixpoint eval_tm