diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index 11fa79be6..c1d617be8 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -17,6 +17,8 @@ Require Import Coq.Relations.Relation_Operators.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Relations.Operators_Properties.
 
+Require Import candid.NamedCases.
+
 Set Bullet Behavior "Strict Subproofs".
 
 Section IDL.
@@ -41,8 +43,8 @@ Section IDL.
   Variable evolves : S -> S -> Prop.
   Notation "s1 ~> s2" := (evolves s1 s2) (at level 70, no associativity).
 
-  Variable hostSubtyping : S -> S -> Prop.
-  Notation "s1 <<: s2" := (hostSubtyping s1 s2) (at level 70, no associativity).
+  Variable hostSubtypeOf : S -> S -> Prop.
+  Notation "s1 <<: s2" := (hostSubtypeOf s1 s2) (at level 70, no associativity).
 
   (* Service Identifiers *)
   Variable I : Set.
@@ -60,36 +62,45 @@ Section IDL.
     (forall i' s, ~ In st (HasRef i' i s)).
 
   Inductive CanSend : State -> I -> T -> T -> I -> Prop :=
-    | CanCall: forall st A B t1 t1' t2 t2',
+    | CanCall:
+      case canCall,
+      forall st A B t1 t1' t2 t2',
       In st (HasRef A B (t1 --> t1')) ->
       In st (HasType B (t2 --> t2')) ->
       CanSend st A t1 t2 B
-    | CanReply: forall st A B t1 t1' t2 t2',
+    | CanReply:
+      case canReply,
+      forall st A B t1 t1' t2 t2',
       In st (HasRef B A (t1 --> t1')) ->
       In st (HasType A (t2 --> t2')) ->
       CanSend st A t2' t1' B.
 
   Inductive step : State -> State -> Prop :=
     | NewService :
+      case newService,
       forall (i : I) (s : S) st,
       FreshIn i st ->
       step st (Add st (HasType i s))
     | EvolveService :
+      case evolveService,
       forall (i : I) (s1 s2 : S) st,
       ~ In st (HasType i s1) ->
       s1 ~> s2 ->
       step (Add st (HasType i s1)) (Add st (HasType i s2))
     | LearnService :
+      case learnService,
       forall (i1 i2 : I) (s: S) st,
       In st (HasType i1 s) ->
       step st (Add st (HasRef i2 i1 s))
     | TransmitService :
+      case transmitService,
       forall (A B C : I) (s1 s2 : S) (t1 t2 : T) st,
       In st (HasRef A C s1) ->
       CanSend st A t1 t2 B ->
       (s1 ∈ t1 <: s2 ∈ t2) ->
       step st (Add st (HasRef B C s2))
     | HostSubtyping :
+      case hostSubtyping,
       forall (A B : I) (s1 s2 : S) st,
       s1 <<: s2 ->
       step (Add st (HasRef A B s1)) (Add st (HasRef A B s2))
@@ -160,11 +171,15 @@ Section IDL.
   Proof.
     intros st Hinvariant.
     intros A t1 t2 B HCanSend.
-    destruct HCanSend.
-    * pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
+    destruct HCanSend; name_cases.
+    [canCall]: {
+      pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
       apply H1.
-    * pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
+    }
+    [canReply]: {
+      pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
       apply H1.
+    }
   Qed.
 
   Lemma invariant_Add_HasType:
@@ -290,8 +305,8 @@ Section IDL.
     forall st1 st2, step st1 st2 -> unique st1 -> unique st2.
   Proof.
     intros st1 st2 Hstep Huniq.
-    induction Hstep.
-    * (* NewService *)
+    induction Hstep; name_cases.
+    [newService]: {
       intros A' s1' s2' HType1 HType2.
       inversion HType1; subst; clear HType1;
       inversion HType2; subst; clear HType2.
@@ -303,7 +318,8 @@ Section IDL.
       - inversion H1; subst; clear H1;
         inversion H0; subst; clear H0.
         reflexivity.
-    * (* EvolveService *)
+    }
+    [evolveService]: {
       intros A' s1' s2' HType1 HType2.
       inversion HType1; subst; clear HType1;
       inversion HType2; subst; clear HType2.
@@ -325,35 +341,41 @@ Section IDL.
       - inversion H1; subst; clear H1;
         inversion H2; subst; clear H0.
         reflexivity.
-    * (* LearnService *)
+    }
+    [learnService]: {
       rewrite unique_Add_HasRef in *.
       assumption.
-    * (* TransmitService *)
+    }
+    [transmitService]: {
       rewrite unique_Add_HasRef in *.
       assumption.
-    * (* HostSubtyping *)
+    }
+    [hostSubtyping]: {
       rewrite unique_Add_HasRef in *.
       assumption.
+    }
   Qed.
 
   Lemma step_preserves_invariant:
     forall st1 st2, step st1 st2 -> unique st1 -> invariant st1 -> invariant st2.
   Proof.
     intros st1 st2 Hstep Huniq Hinv.
-    induction Hstep.
-    * (* NewService *)
+    induction Hstep; name_cases.
+    [newService]: {
       apply invariant_Add_HasType.
       - apply Hinv.
       - intros  B s2 HB.
         eapply H in HB.
         inversion HB.
-    * (* EvolveService *)
+    }
+    [evolveService]: {
       eapply invariant_Change_HasType.
       - apply Hinv.
       - intros B s3 HB Hsub.
         apply evolves_correctly in H0.
         eapply service_subtype_trans; eassumption.
-    * (* LearnService *)
+    }
+    [learnService]: {
       apply invariant_Add_HasRef.
       - apply Hinv.
       - intros s2 HHasType.
@@ -361,7 +383,8 @@ Section IDL.
         replace s2 with s.
         + apply service_subtype_refl.
         + eapply Huniq; eassumption.
-    * (* TransmitService *)
+    }
+    [transmitService]: {
       apply invariant_Add_HasRef.
       - apply Hinv.
       - intros s3 HC.
@@ -370,12 +393,14 @@ Section IDL.
         assert (t1 <: t2) by (eapply HSound; apply H0).
         assert (s1 <:: s2) by (eapply compositional;  eassumption).
         eapply service_subtype_trans; eassumption.
-    * (* HostSubtyping *)
+    }
+    [hostSubtyping]: {
       eapply invariant_Change_HasRef.
       - apply Hinv.
       - intros s3 HB Hsub.
         apply host_subtyping_sound in H.
         eapply service_subtype_trans; eassumption.
+    }
   Qed.
 
   Lemma canonical_soundness: IDLSound.
diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
new file mode 100644
index 000000000..5a3e732d3
--- /dev/null
+++ b/coq/MiniCandid.v
@@ -0,0 +1,661 @@
+(*
+MiniCandid: A formalization of the core ideas of Candid
+*)
+
+Require Import FunInd.
+
+Require Import Psatz.
+
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.Init.Datatypes.
+Require Import Coq.Lists.List.
+
+Require Import Coq.Relations.Relation_Operators.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Operators_Properties.
+
+Set Bullet Behavior "Strict Subproofs".
+Set Default Goal Selector "!".
+
+(* Loads the idiosyncratic CaseNames extension *)
+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) *)
+CoInductive T :=
+  | NatT: T
+  | IntT: T
+  | NullT : T
+  | OptT : T -> T
+  | VecT : T -> T
+  | VoidT : T
+  | ReservedT : T
+  .
+
+Inductive V :=
+  | NatV : nat -> V
+  | IntV : Z -> V
+  | NullV : V
+  | SomeV : V -> V
+  | VecV : list V -> V
+  | ReservedV : V
+  .
+
+(* This 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
+  | OptT _ => true
+  | ReservedT => true
+  | _ => false
+  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. *)
+Inductive HasType : V -> T -> Prop :=
+  | NatHT:
+    case natHT,
+    forall n, NatV n :: NatT
+  | IntHT:
+    case intHT,
+    forall n, IntV n :: IntT
+  | NullHT:
+    case nullHT,
+    NullV :: NullT
+  | NullOptHT:
+    case nullOptHT,
+    forall t, NullV :: OptT t
+  | OptHT:
+    case optHT,
+    forall v t, v :: t -> SomeV v :: OptT t
+  | VecHT:
+    case vecHT,
+    forall vs t, (forall n, n < length vs -> nth n vs NullV :: t) -> VecV vs :: VecT t
+  | 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.
+*)
+
+Reserved Infix "<:" (at level 80, no associativity).
+CoInductive Subtype : T -> T -> Prop :=
+  | ReflST :
+    case reflST,
+    forall t, t <: t
+  | NatIntST :
+    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
+  | VecST :
+    case vecST,
+    forall t1 t2,
+    t1 <: t2 ->
+    VecT t1 <: VecT t2
+  | VoidST :
+    case voidST,
+    forall t, VoidT <: t
+  | ReservedST :
+    case reservedST,
+    forall t, t <: ReservedT
+where "t1 <: t2" := (Subtype t1 t2).
+
+
+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
+  | VecC:
+    case vecC,
+    forall vs1 vs2 t,
+    length vs1 = length vs2 ->
+    (forall n, n < length vs1 -> nth n vs1 NullV ~> nth n vs2 NullV :: t) ->
+    VecV vs1 ~> VecV vs2 :: VecT 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; try (named_constructor; assumption); name_cases.
+  [vecC]: {
+    named_constructor.
+    intros.
+    apply H1. lia.
+  }
+Qed.
+
+Theorem coercion_roundtrip:
+  forall v t, v :: t -> v ~> v :: t.
+Proof.
+  intros. induction H; try (constructor; intuition); name_cases.
+Qed.
+
+Lemma nths_ext:
+  forall A (l1 l2 : list A) d,
+  length l1 = length l2 ->
+  (forall n, n < length l1 -> nth n l1 d = nth n l2 d) ->
+  l1 = l2.
+Proof.
+  intros A l1. induction l1; intros l2 d Heq Hnth.
+  * destruct l2; inversion Heq. reflexivity.
+  * destruct l2; inversion Heq.
+    f_equal.
+    - specialize (Hnth 0 ltac:(simpl;lia)).
+      simpl in Hnth. assumption.
+    - eapply IHl1; try assumption.
+      intros n Hle.
+      specialize (Hnth (S n) ltac:(simpl;lia)).
+      simpl in Hnth. eassumption.
+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);
+    name_cases.
+  [vecC]: {
+    inversion Hother; subst; clear Hother.
+    apply f_equal.
+    eapply nths_ext; try congruence.
+    intros n Hle.
+    apply H1; try congruence.
+    apply H6; 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.
+    eexists. named_econstructor; [constructor|named_constructor].
+  }
+  [optHT_reflST]: {
+    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.
+  }
+  [vecHT_vecST]: {
+    clear H.
+    assert (Hv2 : forall n : nat, n < length vs -> exists v2 : V, nth n vs NullV ~> v2 :: t2) by intuition.
+    clear H0 H2.
+    induction vs.
+    * exists (VecV nil). named_constructor; try reflexivity. intuition. simpl in H. lia.
+    * lapply IHvs.
+      - intros. destruct H as [v2 HC].
+        inversion HC; subst; clear HC.
+        destruct (Hv2 0 ltac:(simpl;lia)) as [va HCa].
+        exists (VecV (va :: vs2)).
+        named_constructor.
+        + simpl; congruence.
+        + intros. simpl in H.
+          destruct n.
+          ** apply HCa.
+          ** apply H3. lia.
+     - intros.
+       specialize (Hv2 (S n) ltac:(simpl;lia)).
+       firstorder.
+  }
+  [vecHT_reflST]: {
+    eexists. named_constructor. 
+    * reflexivity.
+    * intros.
+      apply coercion_roundtrip.
+      apply H.
+      assumption.
+  }
+  [vecHT_constituentOptST]: {
+    inversion H2; subst; clear H2; simpl in H1; inversion H1.
+    * eexists.
+      named_constructor; try reflexivity.
+      named_constructor; try reflexivity.
+      intros. apply coercion_roundtrip. apply H. assumption.
+    * enough (exists v2 : V, VecV vs ~> v2 :: VecT t0)
+        by (destruct H2; eexists; named_constructor; try reflexivity; apply H2).
+      assert (Hv2 : forall n : nat, n < length vs -> exists v2 : V, nth n vs NullV ~> v2 :: t0) by intuition.
+      clear H H0 H1 vecST H4 t.
+      {
+      induction vs.
+      * exists (VecV nil). named_constructor; try reflexivity. intuition. simpl in H. lia.
+      * lapply IHvs.
+        - intros. destruct H as [v2 HC].
+          inversion HC; subst; clear HC.
+          destruct (Hv2 0 ltac:(simpl;lia)) as [va HCa].
+          exists (VecV (va :: vs2)).
+          named_constructor.
+          + simpl; congruence.
+          + intros. simpl in H.
+            destruct n.
+            ** apply HCa.
+            ** apply H3. lia.
+       - intros.
+         specialize (Hv2 (S n) ltac:(simpl;lia)).
+         firstorder.
+       }
+  }
+  [reservedHT_constituentOptST]: {
+    inversion H0; subst; clear H0; simpl in H; inversion H.
+  }
+Qed.
+
+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.
+  cofix Hyp.
+  intros t1 t2 t3 H1 H2.
+  inversion H1; subst; clear H1;
+  inversion H2; subst; clear H2;
+    name_cases;
+    try (constructor; easy).
+  [natIntST_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.
+  }
+  [vecST_vecST0]: {
+    named_constructor.
+    eapply Hyp; eassumption.
+  }
+  [vecST_constituentOptST]: {
+    named_constructor; try assumption.
+    inversion H1; subst; clear H1; try easy.
+    - named_constructor; assumption.
+    - named_constructor. eapply Hyp; eassumption.
+  }
+Qed.
+
+End NoOpportunisticDecoding.
+
+Module OpportunisticDecoding.
+(*
+This is the variant with the opportunistic `t <: opt t'` rule.
+*)
+
+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).
+
+(*
+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).
+
+Definition DoesNotCoerce (v1 : V) (t : T) : Prop := coerce v1 t = None.
+Notation "v1 ~/> :: t" := (DoesNotCoerce v1 t) (at level 80, no associativity).
+
+(*
+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.
+
+Lemma IntC: forall n, IntV n ~> IntV n :: IntT.
+Proof. intros. reflexivity. Qed.
+
+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.
+
+Lemma SomeOptC: forall v1 v2 t,
+    v1 ~> v2 :: t ->
+    SomeV v1 ~> SomeV v2 :: OptT t.
+Proof. unfold Coerces. intros. simpl. rewrite H. reflexivity. Qed.
+
+Lemma OpportunisticOptC:
+    forall v1 t,
+    v1 ~/> :: t ->
+    SomeV v1 ~> NullV :: OptT t.
+Proof.
+  unfold Coerces; unfold DoesNotCoerce. simpl. intros.
+  rewrite H; reflexivity.
+Qed.
+
+Lemma ReservedOptC:
+  forall t, ReservedV ~> NullV :: OptT t.
+Proof. intros. reflexivity. Qed.
+
+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.
+Proof.
+  unfold Coerces. simpl. intros.
+  destruct v1, t; simpl in *; try contradiction; try congruence.
+Qed.
+
+Lemma OpportunisticConstituentOptC:
+    forall v1 t,
+    is_not_opt_like_value v1 ->
+    is_opt_like_type t = false ->
+    v1 ~/> :: t ->
+    v1 ~> NullV :: OptT t.
+Proof.
+  unfold Coerces; unfold DoesNotCoerce. simpl. intros.
+  destruct v1, t; simpl in *; try contradiction; try congruence.
+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.
+*)
+
+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)) ->
+  (case reservedOptC,
+    forall t, P ReservedV NullV (OptT t)) ->
+  (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)) ->
+  (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).
+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.
+Qed.
+
+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.
+  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.
+Qed.
+
+Theorem coercion_roundtrip:
+  forall v t, v :: t -> v ~> v :: t.
+Proof.
+  intros.
+  induction H; try reflexivity.
+  * unfold Coerces in *. simpl. rewrite IHHasType. reflexivity.
+Qed.
+
+Theorem coercion_uniqueness:
+  forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2.
+Proof.
+  intro v.
+  induction v; intros v1 v2 t Heq1 Heq;
+    unfold Coerces in *;
+    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;reflexivity).
+  Show Existentials.
+  [natHT_optST]: {
+    destruct t2; eexists; reflexivity.
+  }
+  [intHT_optST]: {
+    destruct t2; eexists; reflexivity.
+  }
+  [optHT_reflSL]: {
+    specialize (IHHvT t (ReflST _ _)).
+    destruct IHHvT as [v2 Hv2].
+    eexists. unfold Coerces in *. simpl. rewrite Hv2. reflexivity.
+  }
+  [optHT_optST]: {
+    unfold Coerces. simpl.
+    destruct (coerce v t2) eqn:Heq; eexists; reflexivity.
+  }
+Qed.
+
+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.
+  cofix Hyp.
+  intros t1 t2 t3 H1 H2.
+  inversion H1; subst; clear H1;
+  inversion H2; subst; clear H2;
+    name_cases;
+    try (constructor; easy).
+Qed.
+
+End OpportunisticDecoding.
\ No newline at end of file
diff --git a/coq/NamedCases.v b/coq/NamedCases.v
new file mode 100644
index 000000000..685ad714a
--- /dev/null
+++ b/coq/NamedCases.v
@@ -0,0 +1,119 @@
+(** Fun stuff trying to emulate Isar-style case names *)
+
+Inductive CaseName := CaseNameI.
+
+Existing Class CaseName.
+Existing Instance CaseNameI.
+
+From Ltac2 Require Import Ltac2.
+From Ltac2 Require Option.
+Set Default Proof Mode "Classic".
+Ltac name_cases := ltac2:(
+  (* Horribly manual string manipulations. Does this mean I should
+     go to the Ocaml level?
+  *)
+  let strcpy s1 s2 o :=
+    let rec go := fun n =>
+      match Int.lt n (String.length s2) with
+      | true => String.set s1 (Int.add o n) (String.get s2 n); go (Int.add n 1)
+      | false => ()
+      end
+    in go 0
+  in
+  let concat := fun s1 s2 => 
+    let l := Int.add (Int.add (String.length s1) (String.length s2)) 1 in
+    let s := String.make l (Char.of_int 95) in
+    strcpy s s1 0;
+    strcpy s s2 (Int.add (String.length s1) 1);
+    s
+  in
+  Control.enter (let rec go () :=
+    lazy_match! goal with
+    | [ h1 : CaseName, h2 : CaseName |- _ ] =>
+      (* Multiple case names? Combine them (and recurse) *)
+      let h := concat (Ident.to_string h1) (Ident.to_string h2) in
+      Std.clear [h1; h2];
+      let h := Option.get (Ident.of_string h) in
+      assert ($h := CaseNameI);
+      go ()
+    | [ _ : CaseName |- _ ] =>
+      (* A single case name? Set current goal name accordigly. *)
+      ltac1:(
+        (* How to do this in ltac2? *)
+        lazymatch goal with
+        | [ H : CaseName |- _ ] => refine ?[H]; clear H
+        end
+      )
+    | [ |- _ ] =>
+      Control.backtrack_tactic_failure "Did not find any CaseName hypotheses"
+    end
+  in go)
+).
+
+(* To be used instead of constructor when the first assumption is 
+   one of those CaseName assumptions *)
+Ltac clear_names := try exact CaseNameI.
+Ltac named_constructor  := constructor; [ exact CaseNameI | idtac .. ].
+Ltac named_econstructor := econstructor; [ exact CaseNameI | idtac .. ].
+
+Notation "'case' x , t" := (forall {x : CaseName}, t) (at level 200).
+
+Section Example.
+
+  Inductive Test :=
+    | Foo: case foo, Test
+    | Bar: case bar, Test.
+  
+  Goal Test -> Test.
+    intros.
+    destruct H; name_cases.
+    [foo]: {
+      named_constructor.
+    }
+    [bar]: {
+      named_constructor.
+    }
+  Qed.
+  
+  Goal Test -> Test -> Test.
+    intros.
+    destruct H; destruct H0; name_cases.
+    Show Existentials.
+    [foo_foo0]: {
+      named_constructor.
+    }
+    [foo_bar]: {
+      named_constructor.
+    }
+    [bar_foo]: {
+      named_constructor.
+    }
+    [bar_bar0]: {
+      named_constructor.
+    }
+  Qed.
+
+
+  Goal Test -> Test -> Test -> Test.
+    intros.
+    destruct H; destruct H0; destruct H1; name_cases.
+    [foo_foo0_bar]: {
+      named_constructor.
+    }
+    [foo_bar_foo0]: {
+      named_constructor.
+    }
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+  Qed.
+
+  Goal True.
+    (* The tactic fails if it does not find case names *)
+    Fail name_cases.
+  Abort.
+
+End Example.
diff --git a/coq/NamedCasesDemo.v b/coq/NamedCasesDemo.v
new file mode 100644
index 000000000..6f0faf208
--- /dev/null
+++ b/coq/NamedCasesDemo.v
@@ -0,0 +1,201 @@
+(*
+A demo of the NamedCases machinery.
+
+This builds on an example from
+https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html
+and is also explained in
+https://www.joachim-breitner.de/blog/777-Named_goals_in_Coq
+*)
+
+Require Import candid.NamedCases.
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+Inductive reg_exp (T : Type) : Type :=
+| EmptySet
+| EmptyStr
+| Char (t : T)
+| App (r1 r2 : reg_exp T)
+| Union (r1 r2 : reg_exp T)
+| Star (r : reg_exp T).
+Arguments EmptySet {T}.
+Arguments EmptyStr {T}.
+Arguments Char {T} _.
+Arguments App {T} _ _.
+Arguments Union {T} _ _.
+Arguments Star {T} _.
+
+Reserved Notation "s =~ re" (at level 80).
+Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
+  | MEmpty:
+    case empty,
+    [] =~ EmptyStr
+  | MChar:
+    case char,
+    forall x,
+    [x] =~ (Char x)
+  | MApp:
+    case app,
+    forall s1 re1 s2 re2
+    (H1 : s1 =~ re1)
+    (H2 : s2 =~ re2),
+    (s1 ++ s2) =~ (App re1 re2)
+  | MUnionL:
+    case unionL,
+    forall s1 re1 re2
+    (H1 : s1 =~ re1),
+    s1 =~ (Union re1 re2)
+  | MUnionR:
+    case unionR,
+    forall re1 s2 re2
+    (H2 : s2 =~ re2),
+    s2 =~ (Union re1 re2)
+  | MStar0:
+    case star0,
+    forall re,
+    [] =~ (Star re)
+  | MStarApp:
+    case starApp,
+    forall s1 s2 re
+    (H1 : s1 =~ re)
+    (H2 : s2 =~ (Star re)),
+    (s1 ++ s2) =~ (Star re)
+  where "s =~ re" := (exp_match s re).
+
+Lemma star_app0: forall T (s1 s2 : list T) (re : reg_exp T),
+  s1 =~ Star re ->
+  s2 =~ Star re ->
+  s1 ++ s2 =~ Star re.
+Proof.
+  intros T s1 s2 re H1.
+  remember (Star re) as re'.
+   generalize dependent s2.
+  induction H1.
+  - (* MEmpty *) discriminate.
+  - (* MChar *) discriminate.
+  - (* MApp *) discriminate.
+  - (* MUnionL *) discriminate.
+  - (* MUnionR *) discriminate.
+  - (* MStar0 *)
+    injection Heqre' as Heqre''. intros s H. apply H.
+  - (* MStarApp *)
+    injection Heqre' as Heqre''.
+    intros s3 H1. rewrite <- app_assoc.
+    apply MStarApp.
+    + trivial.
+    + apply H1_.
+    + apply IHexp_match2.
+      * rewrite Heqre''. reflexivity.
+      * apply H1.
+Qed.
+
+Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
+  s1 =~ Star re ->
+  s2 =~ Star re ->
+  s1 ++ s2 =~ Star re.
+Proof.
+  intros T s1 s2 re H1.
+  remember (Star re) as re'.
+   generalize dependent s2.
+  induction H1; name_cases; try discriminate.
+  [starApp]: {
+    injection Heqre' as Heqre''.
+    intros s3 H1. rewrite <- app_assoc.
+    apply MStarApp; clear_names.
+    + apply H1_.
+    + apply IHexp_match2.
+      * rewrite Heqre''. reflexivity.
+      * apply H1.
+   }
+  [star0]: {
+    injection Heqre' as Heqre''. intros s H. apply H.
+  }
+Qed.
+
+Inductive Palindrome {T} : list T -> Prop :=
+| EmptyPalin:
+  case emptyP,
+  Palindrome []
+| SingletonPalin:
+  case singletonP,
+  forall x,
+  Palindrome [x]
+| GrowPalin:
+  case growP,
+  forall l x,
+  Palindrome l -> Palindrome ([x] ++ l ++ [x])
+.
+
+Lemma snoc_app_right:
+  forall T (s : list T) re,
+  s =~ Star re ->
+  s = [] \/ (exists s1 s2, s = s1 ++ s2 /\ s1 =~ Star re /\ s2 =~ re).
+Proof.
+  intros T s re H.
+  remember (Star re) as re'.
+  rewrite Heqre'.
+  revert re Heqre'.
+  induction H;
+    intros re' Heq;
+    inversion Heq; subst; clear Heq;
+    name_cases;
+    try (left; reflexivity).
+  [starApp]: {
+    clear IHexp_match1.
+    specialize (IHexp_match2 re' eq_refl).
+    destruct IHexp_match2.
+    - subst.
+      right.
+      exists []. eexists s1.
+      repeat split; try assumption.
+      rewrite app_nil_r. reflexivity.
+    - right.
+      inversion H1 as [s3 [s4 [He1 [Hre1 Hre2]]]]; subst; clear H1.
+      exists (s1 ++ s3). exists s4.
+      repeat split; try assumption.
+      + rewrite app_assoc. reflexivity.
+      + named_constructor; assumption.
+   }
+Qed.
+
+Lemma app_char_char:
+  forall T (x y : T) s,
+  s =~ App (Char x) (Char y) -> s = [x;y].
+Proof.
+  intros.
+  inversion H; subst; clear H.
+  inversion H3; subst; clear H3;
+  inversion H4; subst; clear H4;
+  reflexivity.
+Qed.
+
+Lemma palindrome_star_of_two:
+  forall T (s : list T) a b,
+  Palindrome s -> s =~ Star (App (Char a) (Char b)) ->
+  s = [] \/ a = b.
+Proof.
+  intros T s x y  HPalin HRe.
+  inversion HPalin; inversion HRe; subst; clear HRe; name_cases;
+    try intuition congruence.
+  [singletonP_starApp]: {
+    apply app_char_char in H2; subst.
+    inversion H0.
+  }
+  [growP_starApp]: {
+    right.
+    apply app_char_char in H2; subst.
+    eapply snoc_app_right in H4.
+    inversion H4; subst; clear H4.
+    * rewrite app_nil_r in H3. destruct l; inversion H3; subst; try reflexivity.
+      symmetry in H4.
+      apply app_eq_nil in H4.
+      intuition congruence.
+    * inversion H0 as [s3 [s4 [He1 [Hre1 Hre2]]]]; subst; clear H0.
+      apply app_char_char in Hre2; subst.
+      simpl in H3.
+      inversion H3; subst; clear H3.
+      apply (f_equal (@rev T)) in H2; simpl in *.
+      repeat rewrite ! rev_app_distr in H2; simpl in *.
+      congruence.
+  }
+Qed.
\ No newline at end of file
diff --git a/coq/_CoqProject b/coq/_CoqProject
new file mode 100644
index 000000000..4919bd1fc
--- /dev/null
+++ b/coq/_CoqProject
@@ -0,0 +1 @@
+-Q ./_build/default candid
diff --git a/coq/dune b/coq/dune
index cd6bb06c3..98d3331c0 100644
--- a/coq/dune
+++ b/coq/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name "candid")
  (synopsis "Coq for candid")
- (modules "IDLSoundness")
+ (modules IDLSoundness MiniCandid NamedCases NamedCasesDemo)
 )