diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index c1d617be8..97fcce77e 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -1,13 +1,16 @@
-(* This formalizes
+(**
+
+This theory formalizes
    https://github.com/dfinity/candid/blob/master/spec/IDL-Soundness.md
- *)
+
+*)
 
 Require Import Coq.Lists.List.
 Import ListNotations.
 
 Require Import Coq.Sets.Ensembles.
 (* Odd that this is needed, see
-   https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd
+https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd
 *)
 Arguments In {U}.
 Arguments Add {U}.
@@ -23,16 +26,21 @@ Set Bullet Behavior "Strict Subproofs".
 
 Section IDL.
 
-  (* An abstract theory of IDLs is parametrized as follows: *)
-
-  (* Argument or result types *)
+  (**
+  
+  * The Abstract IDL theory
+  
+  An abstract theory of IDLs is parametrized as follows:
+  *)
+  
+  (** The type of (argument or result types) *)
   Variable T : Set.
 
-  (* A service type is a pair of types *)
+  (** A service type is a pair of types (argument and results) *)
   Definition S : Set := (T * T).
   Notation "t1 --> t2" := (t1, t2) (at level 80, no associativity).
 
-  (* The prediates of the theory *)
+  (** The theory has to define the following predicates *)
   Variable decodesAt : T -> T -> Prop.
   Notation "t1 <: t2" := (decodesAt t1 t2) (at level 70, no associativity).
 
@@ -46,10 +54,10 @@ Section IDL.
   Variable hostSubtypeOf : S -> S -> Prop.
   Notation "s1 <<: s2" := (hostSubtypeOf s1 s2) (at level 70, no associativity).
 
-  (* Service Identifiers *)
+  (** This is generic in the set of service identifiers *)
   Variable I : Set.
 
-  (* Judgements *)
+  (** ** Judgements *)
   Inductive Assertion : Set :=
     | HasType : I -> S -> Assertion
     | HasRef : I -> I -> S -> Assertion.
@@ -108,17 +116,19 @@ Section IDL.
 
   Definition StateSound (st : State) : Prop :=
     forall A t1 t2 B, CanSend st A t1 t2 B ->  t1 <: t2.
+    
+  (** The final soundness proposition *)
 
   Definition IDLSound : Prop :=
     forall s, clos_refl_trans _ step Empty_set s -> StateSound s.
 
-  (* Now we continue with the soundness proof for canonical subtyping.
+  (** * Canonical subtyping *)
 
-     We do so by just adding more hypotheses to this Section.
-     This is fine for now; when we actually want to instantiate this proof
-     with an actual IDL, we may want to revisit this, and maybe
-     modularize this development.
-   *)
+  (**
+  We continue with the soundness proof for canonical subtyping.
+
+  We do so by just adding more hypotheses to this Section.
+  *)
 
   Hypothesis decodesAt_refl: reflexive _ decodesAt.
   Hypothesis decodesAt_trans: transitive _ decodesAt.
@@ -137,7 +147,7 @@ Section IDL.
   Hypothesis host_subtyping_sound:
    forall s1 s2, s1 <<: s2 -> s1 <:: s2.
 
-  (*
+  (**
   Now the actual proofs. When I was writing these, my Coq has become
   pretty rusty, so these are rather manual proofs, with little
   automation. The style is heavily influenced by the explicit Isar-style
diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 6d111c31d..61bfc58d4 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -1,4 +1,4 @@
-(*
+(**
 MiniCandid: A formalization of the core ideas of Candid
 *)
 
@@ -11,6 +11,8 @@ Require Import Coq.Relations.Relation_Operators.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Relations.Operators_Properties.
 
+Require Import Coq.Logic.Decidable.
+
 Set Bullet Behavior "Strict Subproofs".
 Set Default Goal Selector "!".
 
@@ -18,25 +20,48 @@ Set Default Goal Selector "!".
 Require Import candid.NamedCases.
 Set Printing Goal Names. (* Coqide doesn’t use it yet, will be in 8.13 *)
 
-(* Types are coinductive (we do not want to model the graph structure explicilty) *)
+(**
+* Types
+
+We begin by defining the Candid types (or at least some of them).
+
+Candid types are inherently coinductive (e.g. <<type T = opt T>>), so we describe
+them as a coinductive relation. This way we don’t have to model an explicit graph
+structure in Coq.
+*)
 CoInductive T :=
   | NatT: T
   | IntT: T
   | NullT : T
   | OptT : T -> T
+  | FuncT : T -> T -> T
   | VoidT : T
   | ReservedT : T
   .
 
+(**
+* Values
+
+Values are inductive.
+
+We use an unspecified type to model refereneces (could have used [String] too)
+*)
+Axiom RefV : Type.
+
 Inductive V :=
   | NatV : nat -> V
   | IntV : Z -> V
   | NullV : V
   | SomeV : V -> V
+  | FuncV : RefV -> V
   | ReservedV : V
   .
+(**
 
-(* This is a stand in for `null <: t` in places where <: is not allowed yet. *)
+* Typing and subtyping
+
+The following is a stand in for `null <: t` in places where <: is not allowed yet.
+*)
 Definition is_opt_like_type (t : T) : bool :=
   match t with
   | NullT => true
@@ -46,15 +71,7 @@ Definition is_opt_like_type (t : T) : bool :=
   end.
 
 
-Definition is_not_opt_like_value (v : V) : Prop :=
-match v with
-| NullV => False
-| SomeV _ => False
-| ReservedV => False
-| _ => True
-end.
-
-(* The boring, non-subtyping typing relation. *)
+(** The boring, non-subtyping typing relation. *)
 Inductive HasType : V -> T -> Prop :=
   | NatHT:
     case natHT,
@@ -71,42 +88,33 @@ Inductive HasType : V -> T -> Prop :=
   | OptHT:
     case optHT,
     forall v t, v :: t -> SomeV v :: OptT t
+  | FuncHT:
+    case funcHT,
+    forall rv t1 t2, FuncV rv :: FuncT t1 t2
   | ReservedHT:
     case reservedHT,
     ReservedV :: ReservedT
 where "v :: t" := (HasType v t).
 
-
-Module NoOpportunisticDecoding.
-
-(*
-This is the variant without `t <: opt t'`, but with `t <: opt t`.
-Here things are simple and inductive.
-*)
-
+(** The subtyping relation *)
 Reserved Infix "<:" (at level 80, no associativity).
 CoInductive Subtype : T -> T -> Prop :=
   | ReflST :
-    case reflSL,
+    case reflST,
     forall t, t <: t
   | NatIntST :
-    case natIntSL,
+    case natIntST,
     NatT <: IntT
-  | NullOptST :
-    case nullOptST,
-    forall t, NullT <: OptT t
   | OptST :
     case optST,
     forall t1 t2,
-    (* This additional restriction added to fix https://github.com/dfinity/candid/issues/146 *)
-    (is_opt_like_type t1 = is_opt_like_type t2) -> 
-    t1 <: t2 ->
-    OptT t1 <: OptT t2
-  | ConstituentOptST :
-    case constituentOptST,
-    forall t1 t2,
-    is_opt_like_type t2 = false ->
-    t1 <: t2 -> t1 <: OptT t2
+    t1 <: OptT t2
+  | FuncST :
+    case funcST,
+    forall ta1 ta2 tr1 tr2,
+    ta2 <: ta1 ->
+    tr1 <: tr2 ->
+    FuncT ta1 tr1 <: FuncT ta2 tr2
   | VoidST :
     case voidST,
     forall t, VoidT <: t
@@ -115,114 +123,15 @@ CoInductive Subtype : T -> T -> Prop :=
     forall t, t <: ReservedT
 where "t1 <: t2" := (Subtype t1 t2).
 
+(**
+Subtyping is reflexive and transitive.
 
-Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity).
-Inductive Coerces : V -> V -> T -> Prop :=
-  | NatC: 
-    case natC,
-    forall n, NatV n ~> NatV n :: NatT
-  | IntC:
-    case intC,
-    forall n, IntV n ~> IntV n :: IntT
-  | NatIntC:
-    case natIntC,
-    forall n i, i = Z.of_nat n -> (NatV n ~> IntV i :: IntT)
-  | NullC:
-    case nullC,
-    NullV ~> NullV :: NullT
-  | NullOptC:
-    case nullOptC,
-    forall t, NullV ~> NullV :: OptT t
-  | SomeOptC:
-    case someOptC,
-    forall v1 v2 t,
-    v1 ~> v2 :: t ->
-    SomeV v1 ~> SomeV v2 :: OptT t
-  | ConstituentOptC:
-    case constituentC,
-    forall v1 v2 t,
-    is_not_opt_like_value v1 ->
-    v1 ~> v2 :: t ->
-    v1 ~> SomeV v2 :: OptT t
-  | ReservedC:
-    case reservedC,
-    forall v1,
-    v1 ~> ReservedV :: ReservedT
-where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
-
-Lemma is_opt_like_type_correct:
-  forall t,
-  is_opt_like_type t = true <-> NullT <: t.
-Proof.
-  intros. destruct t; simpl; intuition.
-  all: try inversion H.
-  all: try named_constructor.
-Qed.
-
-Theorem coercion_correctness:
-  forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
-Proof.
-  intros. induction H; constructor; assumption.
-Qed.
-
-Theorem coercion_roundtrip:
-  forall v t, v :: t -> v ~> v :: t.
-Proof.
-  intros. induction H; constructor; intuition.
-Qed.
-
-Theorem coercion_uniqueness:
-  forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2.
-Proof.
-  intros.
-  revert v2 H0.
-  induction H; intros v2' Hother;
-    try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence).
-Qed.
-
-Theorem soundness_of_subtyping:
-  forall t1 t2,
-  t1 <: t2 ->
-  forall v1, v1 :: t1 -> exists v2, v1 ~> v2 :: t2.
-Proof.
-  intros t1 t2 Hsub v HvT. revert t2 Hsub.
-  induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
-    name_cases;
-    try (eexists;constructor; try constructor; fail).
-  [natHT_constituentOptST]: {
-    inversion H0; subst; clear H0; simpl in H; inversion H.
-    - eexists. named_constructor; [constructor|named_constructor].
-    - eexists. named_constructor; [constructor|named_constructor;reflexivity].
-  }
-  [intHT_constituentOptST]: {
-    inversion H0; subst; clear H0; simpl in H; inversion H.
-    econstructor. named_econstructor; [constructor|named_constructor].
-  }
-  [optHT_reflSL]: {
-    specialize (IHHvT t (ReflST _ _)).
-    destruct IHHvT as [v2 Hv2].
-    eexists. named_econstructor; try eassumption.
-  }
-  [optHT_optST]: {
-    specialize (IHHvT _ H1).
-    destruct IHHvT as [v2 Hv2].
-    eexists; named_econstructor; eassumption.
-  }
-  [optHT_constituentOptST]: {
-    inversion H0; subst; clear H0; simpl in H; inversion H.
-  }
-  [reservedHT_constituentOptST]: {
-    inversion H0; subst; clear H0; simpl in H; inversion H.
-  }
-Qed.
+Note that these are coinductive proofs! (And yet so neat)
+**)
 
 Theorem subtyping_refl: reflexive _ Subtype.
 Proof. intros x. apply ReflST; constructor. Qed.
 
-Lemma is_not_opt_like_type_contravariant:
-  forall t1 t2,
-     is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false.
-Proof. intros. destruct t1, t2; easy. Qed.
 
 Theorem subtyping_trans: transitive _ Subtype.
 Proof.
@@ -230,313 +139,666 @@ Proof.
   intros t1 t2 t3 H1 H2.
   inversion H1; subst; clear H1;
   inversion H2; subst; clear H2;
-    name_cases;
-    try (constructor; easy).
-  [natIntSL_constituentOptST]: {
-    named_constructor.
-    - assumption.
-    - eapply Hyp; [named_econstructor | assumption].
-  }
-  [optST_optST0]: {
-    named_constructor.
-    - congruence.
-    - eapply Hyp; eassumption.
-  }
-  [optST_constituentOptST]: {
-    inversion H3; subst; clear H3; simpl in H1; congruence.
-  }
-  [constituentOptST_optST]: {
-    named_constructor.
-    - congruence.
-    - firstorder.
-  }
-  [constituentOptST_constituentOptST0]: {
-    inversion H3; subst; clear H3; try easy.
-  }
-  [reservedST_constituentOptST]: {
-    inversion H0; subst; clear H0; inversion H.
-  }
+  constructor; firstorder.
 Qed.
 
-End NoOpportunisticDecoding.
-
-Module OpportunisticDecoding.
-(*
-This is the variant with the opportunistic `t <: opt t'` rule.
+(**
+Subtyping is undecidable, at least the way we model it in Coq.
+But for the decoding function we have to pretend it is decidable.
 *)
+Axiom subtyping_decidable:
+  forall t1 t2, {t1 <: t2} + { ~(t1 <: t2) }.
+Infix "<:?" := subtyping_decidable (at level 80, no associativity).
 
-Reserved Infix "<:" (at level 80, no associativity).
-CoInductive Subtype : T -> T -> Prop :=
-  | ReflST :
-    case reflSL,
-    forall t, t <: t
-  | NatIntST :
-    case natIntSL,
-    NatT <: IntT
-  | OptST :
-    case optST,
-    forall t1 t2,
-    t1 <: OptT t2
-  | VoidST :
-    case voidST,
-    forall t, VoidT <: t
-  | ReservedST :
-    case reservedST,
-    forall t, t <: ReservedT
-where "t1 <: t2" := (Subtype t1 t2).
+Lemma subtype_dec_true:
+  forall T t1 t2 (x y : T), t1 <: t2 -> (if t1 <:? t2 then x else y) = x.
+Proof. intros. destruct (t1 <:? t2); intuition. Qed.
 
-(*
-The coercion relation is not strictly positive, and thus can’t be an inductive
-relations, so we have to implement it as a function that recurses on the value.
-
-This is essentially coercion function, and we can separately try to prove that
-it corresponds to the relation.
- *)
-
-Definition recover x := match x with
-  | None => Some NullV
-  | Some x => Some (SomeV x)
- end.
-
-Function coerce (v1 : V) (t : T) : option V :=
-  match v1, t with
-  | NatV n, NatT => Some (NatV n)
-  | IntV n, IntT => Some (IntV n)
-  | NatV n, IntT => Some (IntV (Z.of_nat n))
-  | NullV, NullT => Some NullV
-  | SomeV v, OptT t => recover (coerce v t)
-  
-  (* This is the rule we would like to have, but 
-     in order to please the termination checker,
-     we have to duplicate all non-opt rules in their opt variant
-  | v, OptT t =>
-    if is_opt_like_type t
-    then None
-    else option_map SomeV (coerce n v t)
-  *)
-  | NatV n, OptT NatT => recover (Some (NatV n))
-  | IntV n, OptT IntT => recover (Some (IntV n))
-  | NatV n, OptT IntT => recover (Some (IntV (Z.of_nat n)))
-  (* OptT never fails (this subsumes NullV and ReservedV) *)
-  | v, OptT _ => Some NullV
-
-  | v, ReservedT => Some ReservedV
-  | v, t => None
-  end.
-  
-Definition Coerces (v1 v2 : V) (t : T) : Prop := coerce v1 t = Some v2.
-Notation "v1 ~> v2 :: t" := (Coerces v1 v2 t) (at level 80, v2 at level 50, no associativity).
+Lemma subtype_dec_false:
+  forall T t1 t2 (x y : T), ~ (t1 <: t2) -> (if t1 <:? t2 then x else y) = y.
+Proof. intros. destruct (t1 <:? t2); intuition. Qed.
 
-Definition DoesNotCoerce (v1 : V) (t : T) : Prop := coerce v1 t = None.
-Notation "v1 ~/> :: t" := (DoesNotCoerce v1 t) (at level 80, no associativity).
+Lemma subtype_dec_refl:
+  forall T t (x y : T), (if t <:? t then x else y) = x.
+Proof. intros. apply subtype_dec_true. named_constructor. Qed. 
 
-(*
-Now we can prove that this indeed implements the inductive relation in the spec:
-*)
+(**
 
-Lemma NatC: forall n, NatV n ~> NatV n :: NatT.
-Proof. intros. reflexivity. Qed.
+* Coercion function
 
-Lemma IntC: forall n, IntV n ~> IntV n :: IntT.
-Proof. intros. reflexivity. Qed.
+The spec defines the coercion function as indexed by the subtyping relation.
+But that relation is coinductive, so Coq will not allow that.
+We thus define the function by recursion on the value.
 
-Lemma NatIntC: forall n i, i = Z.of_nat n -> NatV n ~> IntV i :: IntT.
-Proof. intros. subst. reflexivity. Qed.
-
-Lemma NullC: NullV ~> NullV :: NullT.
-Proof. intros. reflexivity. Qed.
-
-Lemma NullOptC: forall t, NullV ~> NullV :: OptT t.
-Proof. intros. reflexivity. Qed.
+We use [NullV] on the right-hand side in invalid branches.
+*)
 
-Lemma SomeOptC: forall v1 v2 t,
-    v1 ~> v2 :: t ->
-    SomeV v1 ~> SomeV v2 :: OptT t.
-Proof. unfold Coerces. intros. simpl. rewrite H. reflexivity. Qed.
+Function coerce (t1 : T) (t2 : T) (v1 : V) : V :=
+  match v1, t1, t2 with
+  | NatV n, NatT, NatT => NatV n
+  | IntV n, IntT, IntT => IntV n
+  | NatV n, NatT, IntT => IntV (Z.of_nat n)
+  | FuncV r, FuncT ta1 tr1, FuncT ta2 tr2 => FuncV r
+
+  | SomeV v, OptT t1, OptT t2 =>
+    if t1 <:? t2
+    then SomeV (coerce t1 t2 v)
+    else NullV
+  
+  (* We’d prefer the equation from [coerce_constituent_eq] below,
+     but that will not satisfy the termination checker,
+     so let’s repeat all the above ruls for OptT again.
+  *)
+  | NatV n, NatT, OptT NatT => SomeV (NatV n)
+  | IntV n, IntT, OptT IntT => SomeV (IntV n)
+  | NatV n, NatT, OptT IntT => SomeV (IntV (Z.of_nat n))
+  | FuncV r, FuncT ta1 tr1, OptT (FuncT ta2 tr2) =>
+    if ta2 <:? ta1
+    then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV
 
-Lemma OpportunisticOptC:
-    forall v1 t,
-    v1 ~/> :: t ->
-    SomeV v1 ~> NullV :: OptT t.
-Proof.
-  unfold Coerces; unfold DoesNotCoerce. simpl. intros.
-  rewrite H; reflexivity.
-Qed.
+  | v, t, ReservedT => ReservedV
 
-Lemma ReservedOptC:
-  forall t, ReservedV ~> NullV :: OptT t.
-Proof. intros. reflexivity. Qed.
+  (* Failure is NullV. Also subsumes “valid” rules that return NullV *)
+  | _, _, _ => NullV
+  end.
 
-Lemma ConstituentOptC:
-    forall v1 v2 t,
-    is_not_opt_like_value v1 ->
-    is_opt_like_type t = false ->
-    v1 ~> v2 :: t ->
-    v1 ~> SomeV v2 :: OptT t.
+(* We can prove the desired equation at least as an equality *)
+Lemma coerce_constituent_eq:
+  forall v t1 t2,
+  v :: t1 ->
+  is_opt_like_type t1 = false ->
+  coerce t1 (OptT t2) v =
+    if t1 <:? t2
+    then if is_opt_like_type t2
+    then NullV
+    else SomeV (coerce t1 t2 v)
+    else NullV.
 Proof.
-  unfold Coerces. simpl. intros.
-  destruct v1, t; simpl in *; try contradiction; try congruence.
+  intros v t1 t2 HHT His_opt_like.
+  inversion HHT; subst; clear HHT; inversion His_opt_like; clear His_opt_like; name_cases.
+  [natHT]: {
+    destruct (NatT <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl; reflexivity.
+    - destruct t2; try reflexivity; contradict HNotST; named_constructor.
+  }
+  [intHT]: {
+    destruct (IntT <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl; reflexivity.
+    - destruct t2; try reflexivity; contradict HNotST; named_constructor.
+  }
+  [funcHT]: {
+    destruct (FuncT t0 t3 <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl;try reflexivity.
+      * repeat rewrite subtype_dec_refl. reflexivity. 
+      * repeat rewrite subtype_dec_true by assumption. reflexivity. 
+    - destruct t2; try reflexivity.
+      simpl.
+      destruct (t2_1 <:? t0); try reflexivity.
+      destruct (t3 <:? t2_2); try reflexivity.
+      contradict HNotST; named_constructor; assumption.
+  }
 Qed.
 
-Lemma OpportunisticConstituentOptC:
-    forall v1 t,
-    is_not_opt_like_value v1 ->
-    is_opt_like_type t = false ->
-    v1 ~/> :: t ->
-    v1 ~> NullV :: OptT t.
+Lemma coerce_reservedT:
+  forall v t1, coerce t1 ReservedT v = ReservedV.
 Proof.
-  unfold Coerces; unfold DoesNotCoerce. simpl. intros.
-  destruct v1, t; simpl in *; try contradiction; try congruence.
+  intros v1 t1.
+  destruct v1, t1; reflexivity.
 Qed.
 
-Lemma ReservedC: forall v, v ~> ReservedV :: ReservedT.
-Proof. unfold Coerces. intros. destruct v; reflexivity. Qed.
-
-(*
-Now the induction theorem. As always, ugly and bit.
-Note that negative assumptions don’t give you a P predicate.
+(**
+This beast of a lemma defines and proves a nice induction principle for [coerce].
 *)
-
-Lemma Coerces_ind:
-  forall P,
-  (case natC, forall n, P (NatV n) (NatV n) NatT) ->
-  (case intC, forall n, P (IntV n) (IntV n) IntT) ->
-  (case natIntC, forall n, P (NatV n) (IntV (Z.of_nat n)) IntT) ->
-  (case nullC, P NullV NullV NullT) ->
-  (case nullOptC, forall t, P NullV  NullV (OptT t)) ->
-  (case someOptC, forall v1 v2 t,
-    v1 ~> v2 :: t -> P v1 v2 t -> P (SomeV v1) (SomeV v2) (OptT t)) ->
-  (case opportunisticOptC,
-      forall v1 t, v1 ~/> :: t -> P (SomeV v1) NullV (OptT t)) ->
+Lemma coerce_nice_ind:
+  forall (P : T -> T -> V -> V -> Prop),
+  (case natC, forall n, P NatT NatT (NatV n) (NatV n)) ->
+  (case intC, forall n, P IntT IntT (IntV n) (IntV n)) ->
+  (case natIntC, forall n, P NatT IntT (NatV n) (IntV (Z.of_nat n))) ->
+  (case nullC, P NullT NullT NullV NullV) ->
+  (case nullOptC, forall t, P NullT (OptT t) NullV NullV) ->
+  (case optNullC, forall t1 t2, P (OptT t1) (OptT t2) NullV NullV) ->
+  (case optSomeC, forall t1 t2 v1 v2,
+    t1 <: t2 ->
+    v1 :: t1 ->
+    P t1 t2 v1 v2 ->
+    P (OptT t1) (OptT t2) (SomeV v1) (SomeV v2)) ->
+  (case opportunisticOptC, forall t1 t2 v1,
+    ~ (t1 <: t2) ->
+    v1 :: t1 ->
+    P (OptT t1) (OptT t2) (SomeV v1) NullV) ->
   (case reservedOptC,
-    forall t, P ReservedV NullV (OptT t)) ->
+    forall t, P ReservedT (OptT t) ReservedV NullV) ->
   (case constituentOptC,
-    forall v1 v2 t,
-    is_not_opt_like_value v1 ->
-    is_opt_like_type t = false ->
-    v1 ~> v2 :: t ->
-    P v1 v2 t -> 
-    P v1 (SomeV v2) (OptT t)) ->
+    forall t1 t2 v1 v2,
+    (* The following assumption is redundant, as it follows from the
+       two subsequent onces, but it is convenient when using this
+       induction theorem *)
+    is_opt_like_type t1 = false ->
+    is_opt_like_type t2 = false ->
+    t1 <: t2 ->
+    v1 :: t1 ->
+    P t1 t2 v1 v2 ->
+    P t1 (OptT t2) v1 (SomeV v2)) ->
   (case opportunisticConstituentOptC,
-    forall v1 t,
-    is_not_opt_like_value v1 ->
-    is_opt_like_type t = true \/ v1 ~/> :: t ->
-    P v1 NullV (OptT t)) ->
-  (case reservedC, forall v, P v ReservedV ReservedT) ->
-  (forall v1 v2 t, v1 ~> v2 :: t -> P v1 v2 t).
+    forall t1 t2 v1,
+    v1 :: t1 ->
+    is_opt_like_type t1 = false ->
+    is_opt_like_type t2 = true \/ ~ (t1 <: t2) ->
+    P t1 (OptT t2) v1 NullV) ->
+  (case funcC, forall ta1 tr1 ta2 tr2 v,
+    ta2 <: ta1 ->
+    tr1 <: tr2 ->
+    P (FuncT ta1 tr1) (FuncT ta2 tr2) (FuncV v) (FuncV v)) ->
+  (case reservedC, forall t v, v :: t -> P t ReservedT v ReservedV) ->
+  (forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> P t1 t2 v1 (coerce t1 t2 v1)).
 Proof.
-  unfold Coerces. unfold DoesNotCoerce.
-  intros P NatC IntC NatIntC NullC NullOptC SomeOptC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC ReservedC v1.
-  induction v1; intros v2 t Hcoerces; destruct t.
-  all: try (inversion Hcoerces; subst; clear Hcoerces; intuition; fail). 
-  all: simpl in Hcoerces.
-  * destruct t;
-    inversion Hcoerces; subst; clear Hcoerces.
-    + apply ConstituentOptC; clear_names; simpl; intuition.
-    + apply ConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
-  * destruct t;
-    inversion Hcoerces; subst; clear Hcoerces.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
-    + apply ConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
-    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
-  * destruct (coerce v1 t) eqn:Heq; simpl in Hcoerces;
-    inversion Hcoerces; subst; clear Hcoerces.
-    + apply SomeOptC; clear_names; intuition.
-    + apply OpportunisticOptC; clear_names; easy.
+  intros P.
+  intros NatC IntC NatIntC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC FuncC ReservedC.
+  intros t1 t2 v1 HST HHT.
+  revert t2 HST.
+  induction HHT; name_cases.
+  [natHT]: {
+    intros. 
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply NatC; clear_names. }
+    [natIntST]: { apply NatIntC; clear_names. }
+    [optST]: {
+      (* oddly,
+        rewrite coerce_constituent_eq by (try named_constructor; reflexivity).
+        does not seem to lead to a simpler proof here.
+      *)
+      destruct (is_opt_like_type t0) eqn:His_opt_like.
+      * destruct t0; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable NatT t0).
+        + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+        + destruct t0; inversion His_opt_like; clear His_opt_like.
+          - contradict n0. named_constructor.
+          - contradict n0. named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [intHT]: {
+    intros. 
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply IntC; clear_names. }
+    [optST]: {
+      destruct (is_opt_like_type t0) eqn:His_opt_like.
+      * destruct t0; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable IntT t0).
+        + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+        + destruct t0; inversion His_opt_like; clear His_opt_like.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - contradict n0. named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [funcHT]: {
+    intros. 
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply FuncC; clear_names; apply ReflST; clear_names. }
+    [optST]: {
+      destruct (is_opt_like_type t4) eqn:His_opt_like.
+      * destruct t4; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable (FuncT t1 t2) t4).
+        + destruct t4; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - simpl. repeat rewrite subtype_dec_refl.
+            apply ConstituentOptC; clear_names; simpl; try (intuition;fail).
+            ** apply ReflST; clear_names; apply ReflST; clear_names.
+            ** named_constructor.
+            ** apply FuncC; clear_names; apply ReflST; clear_names.
+          - simpl. repeat rewrite subtype_dec_true by assumption.
+            apply ConstituentOptC; clear_names; simpl; try (intuition;fail).
+            ** named_constructor; assumption.
+            ** named_constructor.
+        + destruct t4; inversion His_opt_like; clear His_opt_like.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - simpl.
+            destruct (t4_1 <:? t1).
+            ** destruct (t2 <:? t4_2).
+               ++ contradict n. named_constructor; assumption.
+               ++ apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+            ** apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [funcST]: { apply FuncC; clear_names; assumption. }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [nullHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply NullC; clear_names. }
+    [optST]: { apply NullOptC; clear_names. }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [nullOptHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply OptNullC; clear_names. }
+    [optST]: { apply OptNullC; clear_names. }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [optHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: {
+      simpl.
+      destruct (t <:? t) as [HST | HNoST].
+      * apply OptSomeC; clear_names; intuition.
+      * contradict HNoST. apply ReflST; clear_names.
+    }
+    [optST]: {
+      simpl. 
+      destruct (t <:? t0) as [HST | HNoST].
+      * apply OptSomeC; clear_names; intuition.
+      * apply OpportunisticOptC; clear_names; intuition.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor; assumption. }
+  }
+  [reservedHT]: { 
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply ReservedC; clear_names. named_constructor. }
+    [optST]: { apply ReservedOptC; clear_names. }
+    [reservedST]: { apply ReservedC; clear_names.  named_constructor. }
+  }
 Qed.
 
-Lemma is_opt_like_type_correct:
-  forall t,
-  is_opt_like_type t = true <-> NullT <: t.
+(**
+* Properties of coercion
+
+Round-tripping
+*)
+Lemma coerce_roundtrip:
+  forall t1 v1,
+  v1 :: t1 ->
+  coerce t1 t1 v1 = v1.
 Proof.
-  intros. destruct t; simpl; intuition.
-  all: try inversion H.
-  all: try named_constructor.
+  enough (forall t1 t2 v1,
+    t1 <: t2 -> v1 :: t1 -> t2 = t1 ->
+    coerce t1 t2 v1 = v1)
+    by (intros; apply H; intuition; try apply ReflST; clear_names).
+  apply (coerce_nice_ind (fun t1 t2 v1 v2 => t2 = t1 -> v2 = v1));
+    intros; name_cases; try solve [subst; simpl in *; congruence].
+  [optSomeC]: {apply f_equal. apply H1. congruence. }
+  [opportunisticOptC]: {
+    inversion H1; subst; clear H1. contradiction H; apply ReflST; clear_names.
+  }
+  [reservedC]: {  inversion H; subst; clear H; congruence. }
 Qed.
 
-Theorem coercion_correctness:
-  forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
+(**
+Coercion does not fail (and is well-defined)
+*)
+
+Lemma coerce_well_defined:
+  forall t1 t2 v1,
+  t1 <: t2 -> v1 :: t1 ->
+  coerce t1 t2 v1 :: t2.
 Proof.
-  intros.
-  revert v2 t H.
-  induction v1;
-  intros v2 t Hcoerce;
-    unfold Coerces in Hcoerce;
-    functional inversion Hcoerce; simpl in *; subst; clear Hcoerce;
-    try (named_constructor; named_constructor; fail).
-  * destruct (coerce v1 t1) eqn:Heq; simpl in *; inversion H0; subst; clear H0.
-    - specialize (IHv1 _ _ Heq).
-      named_constructor; assumption. 
-    - named_constructor.
+  apply coerce_nice_ind with (P := fun t1 t2 v1 v2 => v2 :: t2); intros; name_cases;
+     named_constructor; assumption.
 Qed.
 
-Theorem coercion_roundtrip:
-  forall v t, v :: t -> v ~> v :: t.
+
+(**
+* IDL Soundess 
+
+To work towards IDL soundness, we need a predicate for “Value v contains
+a function reference at function type t.”. Moreover, this contains
+relation should indicate the position in the value in a way that
+the positions match up even after coercions.
+
+So we start by giving names to positions
+(This needs to be extended once we have sequences and records)
+*)
+Inductive Path :=
+  | Here : Path
+  | The : Path -> Path
+  .
+
+(**
+And a function that finds the value at a given path.
+
+It returns [None] if the path does not make sense for this value.
+*)
+Fixpoint val_idx (p : Path) (v : V) : option V :=
+  match p with
+  | Here => Some v
+  | The p =>
+    match v with
+    | SomeV v => val_idx p v
+    | _ => None
+    end
+  end.
+
+(**
+This is a lenient variant, which is total (returning [NullV]
+when the path is invalid), which makes proofs simpler.
+
+It also ignores extra [The] on the path; this way one can 
+use this on the pre-coerced value, and get the right value,
+even if the constituent-to-optional rule was used.
+*)
+Fixpoint val_idx' (p : Path) (v : V) : V :=
+  match p with
+  | Here => v
+  | The p =>
+    match v with
+    | SomeV v => val_idx' p v
+    | NullV => NullV
+    | ReservedV => NullV
+    | _ => val_idx' p v
+    end
+  end.
+
+(**
+The corresponding function for types, also lenient.
+*)
+Fixpoint typ_idx' (p : Path) (t : T) : T :=
+  match p with
+  | Here => t
+  | The p =>
+    match t with
+    | OptT t => typ_idx' p t
+    | NullT => VoidT
+    | ReservedT => VoidT
+    | _ => typ_idx' p t
+    end
+  end.
+
+(**
+Properties about [val_idx] and [typ_idx'], mostly for sanity-checking
+*)
+Lemma path_preserves_types:
+  forall v v' t p,
+  v :: t ->
+  val_idx p v = Some v' ->
+  v' :: typ_idx' p t.
 Proof.
-  intros.
-  induction H; try reflexivity.
-  * unfold Coerces in *. simpl. rewrite IHHasType. reflexivity.
+  intros v v' t p.
+  revert v v' t.
+  induction p.
+  * intros v v' t HHT Hval_idx.
+    inversion Hval_idx; subst; clear Hval_idx.
+    assumption.
+  * intros v v' t HHT Hval_idx.
+    inversion Hval_idx; subst; clear Hval_idx.
+    inversion HHT; subst; clear HHT; name_cases.
+    all: firstorder congruence.
 Qed.
 
-Theorem coercion_uniqueness:
-  forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2.
+Lemma val_idx_is_val_idx':
+  forall v v' t p,
+  v :: t ->
+  val_idx p v = Some v' ->
+  val_idx' p v = v'.
 Proof.
-  intro v.
-  induction v; intros v1 v2 t Heq1 Heq;
-    unfold Coerces in *;
-    congruence.
+  intros v v' t p.
+  revert v v' t.
+  induction p.
+  * intros v v' t HHT Hval_idx.
+    inversion Hval_idx; subst; clear Hval_idx.
+    reflexivity.
+  * intros v v' t HHT Hval_idx.
+    inversion Hval_idx; subst; clear Hval_idx.
+    inversion HHT; subst; clear HHT; name_cases.
+    all: firstorder congruence.
 Qed.
 
-Theorem soundness_of_subtyping:
-  forall t1 t2,
+(**
+The core lemma towards compositionality:
+
+All values in a decoded value originate from a value in the original value,
+and their types are related.
+
+This may be proving a bit more than needed for compositionality, but it my be
+handy for other things.
+*)
+
+Lemma no_new_values:
+  forall t1 t2 v1,
   t1 <: t2 ->
-  forall v1, v1 :: t1 -> exists v2, v1 ~> v2 :: t2.
+  v1 :: t1 ->
+  forall p iv2,
+  val_idx p (coerce t1 t2 v1) = Some iv2 ->
+    (iv2 = NullV \/ typ_idx' p t1 <: typ_idx' p t2) /\
+    val_idx' p v1 :: typ_idx' p t1 /\
+    coerce (typ_idx' p t1) (typ_idx' p t2) (val_idx' p v1) = iv2.
 Proof.
-  intros t1 t2 Hsub v HvT. revert t2 Hsub.
-  induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
-    name_cases;
-    try (eexists;reflexivity).
-  Show Existentials.
-  [natHT_optST]: {
-    destruct t2; eexists; reflexivity.
+  apply (coerce_nice_ind (fun t1 t2 v1 v2 =>
+    forall p iv2,
+    forall (Hval_idx : val_idx p v2 = Some iv2),
+      (iv2 = NullV \/ typ_idx' p t1 <: typ_idx' p t2) /\
+      val_idx' p v1 :: typ_idx' p t1 /\
+      coerce (typ_idx' p t1) (typ_idx' p t2) (val_idx' p v1) = iv2
+  )); intros; name_cases.
+  all:
+    try solve [destruct p; inversion Hval_idx; subst; clear Hval_idx; intuition (named_constructor; assumption)].
+  [optSomeC]: {
+    destruct p; inversion Hval_idx; subst; clear Hval_idx.
+    * specialize (H1 Here v2 eq_refl).
+      simpl in *.
+      decompose record H1; clear H1.
+      repeat split.
+      - right; named_constructor; assumption.
+      - named_constructor; assumption.
+      - simpl. rewrite subtype_dec_true by assumption. congruence.
+    * specialize (H1 _ _ H3).
+      intuition.
   }
-  [intHT_optST]: {
-    destruct t2; eexists; reflexivity.
+  [opportunisticOptC]: {
+    destruct p; inversion Hval_idx; subst; clear Hval_idx.
+    simpl in *.
+    repeat split.
+    - left; reflexivity.
+    - named_constructor. assumption.
+    - simpl. rewrite subtype_dec_false by assumption. reflexivity.
   }
-  [optHT_reflSL]: {
-    specialize (IHHvT t (ReflST _ _)).
-    destruct IHHvT as [v2 Hv2].
-    eexists. unfold Coerces in *. simpl. rewrite Hv2. reflexivity.
+  [constituentOptC]: {
+    destruct p; inversion Hval_idx; subst; clear Hval_idx.
+    * specialize (H3 Here v2 eq_refl).
+      simpl in *.
+      decompose record H3; clear H3.
+      repeat split.
+      - right;  named_constructor.
+      - assumption.
+      - rewrite coerce_constituent_eq by assumption.
+        rewrite H0.
+        rewrite subtype_dec_true by assumption. congruence.
+    * specialize (H3 _ _ H5).
+      decompose record H3; clear H3.
+      inversion H2; subst; clear H2; inversion H; subst; clear H; intuition.
   }
-  [optHT_optST]: {
-    unfold Coerces. simpl.
-    destruct (coerce v t2) eqn:Heq; eexists; reflexivity.
+  [opportunisticConstituentOptC]: {
+    destruct p; inversion Hval_idx; subst; clear Hval_idx.
+    simpl in *.
+    repeat split.
+    - left; reflexivity.
+    - assumption.
+    - rewrite coerce_constituent_eq by assumption.
+      destruct H1.
+      * rewrite H1. destruct (t1 <:? t2); reflexivity.
+      * rewrite subtype_dec_false by assumption. reflexivity.
+  }
+  [reservedC]: {
+    destruct p; inversion Hval_idx; subst; clear Hval_idx.
+    simpl in *.
+    repeat split.
+    - right; named_constructor; assumption.
+    - assumption.
+    - destruct t, v; simpl; try reflexivity.
   }
 Qed.
 
-Theorem subtyping_refl: reflexive _ Subtype.
-Proof. intros x. apply ReflST; constructor. Qed.
+(**
+This is the instantiation of [passesThrough] from the IDL-Soundness theory.
+*)
+Definition passesThrough (s1 : T * T) (t1 : T) (s2 : T * T) (t2 : T) :=
+  exists v1 p r,
+  v1 :: t1 /\
+  val_idx' p v1 = FuncV r /\
+  typ_idx' p t1 = FuncT (fst s1) (snd s1) /\
+  val_idx  p (coerce t1 t2 v1) = Some (FuncV r) /\
+  typ_idx' p t2 = FuncT (fst s2) (snd s2).
+
+(**
+And indeed subtyping is compositional:
+*)
+Lemma compositional:
+  forall t1 t2 s1 s2,
+  t1 <: t2 -> passesThrough s1 t1 s2 t2 -> (snd s1 <: snd s2 /\ fst s2 <: fst s1).
+Proof.
+  intros.
+  unfold passesThrough in *.
+  destruct s1, s2.
+  simpl in *.
+  enough (FuncT t t0 <: FuncT t3 t4)
+    by (inversion H1; subst; clear H1; split; try assumption; named_constructor).
+  destruct H0 as [v1 [p [r Hpt]]].
+  decompose record Hpt; clear Hpt.
+  pose proof (no_new_values t1 t2 v1 H H0 p _ H3) as Hnnv.
+  decompose record Hnnv; clear Hnnv.
+  destruct H4; congruence.
+Qed.
 
-Lemma is_not_opt_like_type_contravariant:
-  forall t1 t2,
-  is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false.
-Proof. intros. destruct t1, t2; easy. Qed.
+(**
+Now we can instantiate the soundness theorem from IDLSoundness
+*)
 
-Theorem subtyping_trans: transitive _ Subtype.
+Require Import candid.IDLSoundness.
+
+Theorem soundness:
+  forall I,
+  IDLSound T Subtype passesThrough
+    (fun '(ta2, tr2) '(ta1,tr1)  => ta2 <: ta1 /\ tr1 <: tr2)
+    (fun '(ta1,tr1) '(ta2, tr2) => ta2 <: ta1 /\ tr1 <: tr2)
+    I.
 Proof.
-  cofix Hyp.
-  intros t1 t2 t3 H1 H2.
-  inversion H1; subst; clear H1;
-  inversion H2; subst; clear H2;
-    name_cases;
-    try (constructor; easy).
+  intro.
+  apply canonical_soundness.
+  - apply subtyping_refl.
+  - apply subtyping_trans.
+  - unfold service_subtyping.
+    intros.
+    destruct s1 as [ta1 tr1].
+    destruct s2 as [ta2 tr2].
+    intuition.
+  - intros.
+    pose proof (compositional _ _ _ _ H H0).
+    unfold service_subtyping.
+    intros.
+    destruct s1 as [ta1 tr1].
+    destruct s2 as [ta2 tr2].
+    intuition.
+  - intros.
+    destruct s1 as [ta1 tr1].
+    destruct s2 as [ta2 tr2].
+    unfold service_subtyping.
+    intuition.
 Qed.
 
-End OpportunisticDecoding.
\ No newline at end of file
+(**
+* Transitive coherence
+
+Transitive coherence only holds up to a weaker relation:
+*)
+
+Reserved Infix "~~" (at level 80, no associativity).
+CoInductive UpToNull : V -> V -> Prop :=
+  (* This is the interesting rule: *)
+  | NullSomeUT:
+    forall v,
+    NullV ~~ SomeV v
+  | SomeNullUT:
+    forall v,
+    SomeV v ~~ NullV
+    
+  (* The rest just form the homomorphic closure *)
+  | NatUT:
+    forall n, NatV n ~~ NatV n
+  | IntUT:
+    forall n, IntV n ~~ IntV n
+  | NullUT:
+    NullV ~~ NullV
+  | SomeUT:
+    forall v1 v2,
+    v1 ~~ v2 ->
+    SomeV v1 ~~ SomeV v2
+  | FuncUT:
+    forall r, FuncV r ~~ FuncV r
+  | ReservedUT:
+    ReservedV ~~ ReservedV
+where "v1 ~~ v2" := (UpToNull v1 v2).
+
+Lemma UpToNull_refl:
+  forall v, UpToNull v v.
+Proof. intros. induction v; constructor; assumption. Qed.
+
+(** A small tactic that I keep copying into each development *)
+Ltac destruct_match :=
+  match goal with
+  | [ H :context[match ?a with _ => _ end] |- _] =>
+    let Heq := fresh "Heq" in
+    destruct a eqn:Heq
+  | [ |- context[match ?a with _ => _ end]] =>
+    let Heq := fresh "Heq" in
+    destruct a eqn:Heq
+  end.
+
+Theorem transitive_coherence:
+  forall ta tb tc v1,
+  ta <: tb ->
+  tb <: tc ->
+  v1 :: ta ->
+  coerce tb tc (coerce ta tb v1) ~~ coerce ta tc v1.
+Proof.
+  intros ta tb tc v1 HST1 HST2 HHT.
+  revert tc HST2.
+  revert ta tb v1 HST1 HHT.
+  apply (coerce_nice_ind (fun ta tb v1 v2 =>
+    forall tc : T,
+     forall HST2 : tb <: tc,
+      coerce tb tc v2 ~~ coerce ta tc v1
+  )); intros; inversion HST2; subst; clear HST2.
+  all: simpl.
+  all: try rewrite coerce_constituent_eq by assumption.
+  all: try rewrite coerce_reservedT.
+  all: try rewrite subtype_dec_refl.
+  all: try rewrite subtype_dec_true by assumption.
+  all: try solve [
+    repeat destruct_match;
+    try apply UpToNull_refl;
+    intuition constructor
+    ].
+  all: name_cases.
+  [optSomeC_reflST]: { constructor. apply H1. named_constructor. }
+  [optSomeC_optST]: {
+    repeat destruct_match; try apply UpToNull_refl; try  apply NullSomeUT.
+    - constructor. apply H1. assumption.
+    - contradiction n. eapply subtyping_trans; eassumption.
+  }
+  [constituentOptC_reflST]: {
+    rewrite H0.
+    constructor. apply H3. named_constructor.
+  }
+  [constituentOptC_optST]: {
+    repeat destruct_match; try apply UpToNull_refl; try  apply NullSomeUT.
+    - constructor.
+    - constructor. apply H3. assumption.
+    - contradiction n. eapply subtyping_trans; eassumption.
+  }
+  [reservedC_optST]: {
+    destruct t, v; simpl; repeat destruct_match; try apply UpToNull_refl; try  apply NullSomeUT.
+  } 
+Qed.