diff --git a/case-studies/classical-processes/LICENSE b/case-studies/classical-processes/LICENSE
new file mode 100644
index 000000000..c35a8adab
--- /dev/null
+++ b/case-studies/classical-processes/LICENSE
@@ -0,0 +1,13 @@
+Copyright 2023 Chuta Sano, Ryan Kavanagh, Brigitte Pientka
+
+Permission to use, copy, modify, and/or distribute this software for any purpose
+with or without fee is hereby granted, provided that the above copyright notice
+and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED “AS IS” AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH
+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,
+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS
+OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER
+TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF
+THIS SOFTWARE.
diff --git a/case-studies/classical-processes/README.md b/case-studies/classical-processes/README.md
new file mode 100644
index 000000000..6adfe8aed
--- /dev/null
+++ b/case-studies/classical-processes/README.md
@@ -0,0 +1,95 @@
+# Overview
+
+This artifact contains the Beluga mechanization for the paper
+
+    Mechanizing Session-Types Using a Structural View
+    C. Sano, R. Kavanagh, B. Pientka
+    Proceedings of the ACM on Programming Languages, Volume 7,
+    Number OOPSLA2, Article No. 235 (October 2023),
+    https://doi.org/10.1145/3622810
+
+and is a copy of the accompanying artifact (https://doi.org/10.5281/zenodo.8329645)
+
+Below are files that are included in this artifact.
+
+	cp.cfg         - Collects all used Beluga source files
+	cp_base.bel    - Contains encodings of session types and processes
+	cp_linear.bel  - Contains encoding of the linearity predicate
+	cp_statics.bel - Contains encoding of the type judgment
+	cp_dyn.bel     - Contains encoding of the reductions and congruences
+	cp_lemmas.bel  - Contains proofs of intermediary lemmas
+	cp_thrm.bel    - Proof of type preservation
+
+There are some minor differences in code snippets as written in the
+paper for presentation purposes compared to the code in the artifact,
+which we summarize below.
+
+| Item                    | On-paper Notation | Artifact     |
+|-------------------------|-------------------|--------------|
+| Reduction rule names    | βcut1 and βinl    | β∥1 and β⊕&1 |
+| Structural Equivalences | equiv P Q         | P ≡ Q        |
+| Reductions              | step P Q          | P ⇛ Q        |
+| Abstractions            | λx. M             | \x. M        |
+
+## Paper to Artifact Table
+
+| Definition/Proofs                                     | Paper                        | File           | Definition Name                                    |
+|-------------------------------------------------------|------------------------------|----------------|----------------------------------------------------|
+| Session types, duality, and processes                 | Sections 4.1 and 4.2         | cp_base.bel    | tp, dual, and proc                                 |
+| Linearity predicate                                   | Section 4.3                  | cp_linear.bel  | linear                                             |
+| Type judgments                                        | Section 4.4                  | cp_statics.bel | wtp                                                |
+| Reductions and Structural Equivalences                | Section 4.5                  | cp_dyn.bel     | ⇛ and ≡ (used as infix operators)                  |
+| Symmetricity and Uniqueness of dual                   | Section 6.1                  | cp_lemmas.bel  | dual_sym and dual_uniq                             |
+| Strengthening Lemmas                                  | Section 6.2, Lemma 6.1 (1-5) | cp_lemmas.bel  | str_hyp, str_lin, str_wtp, str_step, and str_equiv |
+| Linearity implies usage                               | Section 6.3, Lemma 6.2       | cp_lemmas.bel  | lin_name_must_appear                               |
+| Structural equivalence preserves linearity and typing | Section 6.3, Lemma 6.3       | cp_thrm.bel    | lin_s≡ and wtp_s≡                                  |
+| Type preservation                                     | Section 6.4, Theorem 6.4     | cp_thrm.bel    | lin_s and wtp_s                                    |
+
+
+# Installation and Execution
+
+This mechanization is compatible with Beluga version 1.1.
+
+## Installation
+
+The easiest way to install Beluga is using `opam`:
+
+    >> opam install beluga.1.1
+
+Beluga can also be installed from source by following the "Installation
+from the source" instructions on
+https://github.com/Beluga-lang/Beluga/tree/v1.1
+
+Alternatively, we have provided a virtual machine based on OpenBSD 7.3
+that has Beluga 1.1, its sources, and our mechanization pre-installed.
+This QCOW2 disk image can be run using QEMU using the command:
+
+    >> qemu-system-amd64 -hda artifact.qcow2 -m 1G
+
+For a better user experience, we suggest the following options, which
+give the virtual machine 4 gigabytes of memory, four CPUs, and allow
+the machine to be accessed over SSH on localhost port 60022 using
+username `artifact` and password `artifact`:
+
+    >> qemu-system-amd64 -hda artifact.qcow2 -m 4G -smp 4 \
+                         -nic user,hostfwd=tcp::60022-:22
+    >> ssh artifact@127.0.0.1 -p 60022
+
+## Execution
+
+Once Beluga is installed, it can be run on the file `cp.cfg`. The
+following is the expected output:
+
+	>> beluga cp.cfg
+	## Type Reconstruction begin: ./cp_base.bel ##
+	## Type Reconstruction done:  ./cp_base.bel ##
+	## Type Reconstruction begin: ./cp_linear.bel ##
+	## Type Reconstruction done:  ./cp_linear.bel ##
+	## Type Reconstruction begin: ./cp_statics.bel ##
+	## Type Reconstruction done:  ./cp_statics.bel ##
+	## Type Reconstruction begin: ./cp_dyn.bel ##
+	## Type Reconstruction done:  ./cp_dyn.bel ##
+	## Type Reconstruction begin: ./cp_lemmas.bel ##
+	## Type Reconstruction done:  ./cp_lemmas.bel ##
+	## Type Reconstruction begin: ./cp_thrm.bel ##
+	## Type Reconstruction done:  ./cp_thrm.bel ##
diff --git a/case-studies/classical-processes/cp.cfg b/case-studies/classical-processes/cp.cfg
new file mode 100644
index 000000000..a7120e93a
--- /dev/null
+++ b/case-studies/classical-processes/cp.cfg
@@ -0,0 +1,7 @@
+cp_base.bel
+cp_linear.bel
+cp_statics.bel
+cp_dyn.bel
+cp_lemmas.bel
+cp_thrm.bel
+
diff --git a/case-studies/classical-processes/cp_base.bel b/case-studies/classical-processes/cp_base.bel
new file mode 100644
index 000000000..60657c182
--- /dev/null
+++ b/case-studies/classical-processes/cp_base.bel
@@ -0,0 +1,49 @@
+% Basic shared definitions of CP
+% Defines types, duality, processes, and equality predicates on types/processes
+
+name : type.      % channel names
+
+tp : type.        % channel types
+① : tp.           % termination ("provider")
+⊥ : tp.           % termination ("client")
+⊗ : tp → tp → tp. % channel output
+⅋ : tp → tp → tp. % channel input
+& : tp → tp → tp. % receive choice
+⊕ : tp → tp → tp. % send choice
+
+--infix ⊗ 5 left.
+--infix ⅋ 5 left.
+--infix ⊕ 4 left.
+--infix & 4 left.
+
+eq : tp → tp → type.
+refl : eq A A.
+
+% duality condition
+dual : tp → tp → type.
+D1 : dual ① ⊥.
+D⊥ : dual ⊥ ①.
+D⊗ : dual A A' → dual B B' → dual (A ⊗ B) (A' ⅋ B').
+D⅋ : dual A A' → dual B B' → dual (A ⅋ B) (A' ⊗ B').
+D& : dual A A' → dual B B' → dual (A & B) (A' ⊕ B').
+D⊕ : dual A A' → dual B B' → dual (A ⊕ B) (A' & B').
+
+% processes
+proc : type.
+
+eq_proc : proc → proc → type.
+refl_proc : eq_proc P P.
+
+fwd : name → name → proc.                             % fwd x y
+pcomp : tp → (name → proc) → (name → proc) → proc.    % nu x:A (P | Q)
+
+close : name → proc.                                  % close x
+wait : name → proc → proc.                            % wait x; P
+
+out : name → (name → proc) → (name → proc) → proc.    % out x; (y.P | w.Q)
+inp : name → (name → name → proc) → proc.             % inp x; w.y.P
+
+inl : name → (name → proc) → proc.                    % x[inl]; w.P
+inr : name → (name → proc) → proc.                    % x[inr]; w.P
+choice : name → (name → proc) → (name → proc) → proc. % case x {w.P | w.Q}
+
diff --git a/case-studies/classical-processes/cp_dyn.bel b/case-studies/classical-processes/cp_dyn.bel
new file mode 100644
index 000000000..995f7272f
--- /dev/null
+++ b/case-studies/classical-processes/cp_dyn.bel
@@ -0,0 +1,52 @@
+% Dynamics of CP
+
+% Structural Equivalences
+≡ : proc → proc → type.
+--infix ≡ 10 left.
+≡comm : dual A A' → (pcomp A  P Q) ≡ (pcomp A' Q  P).
+≡assoc: (pcomp B (\y. pcomp A P (\x. Q x y)) R)
+      ≡ (pcomp A P (\x. pcomp B (Q x) R)).
+
+% Beta reductions, commuting conversions, and congruence for pcomp
+⇛ : proc → proc → type.
+--infix ⇛ 10 left.
+
+% Note: keep in mind ⇛ is an infix type constructor and is therefore unrelated to
+% →, which constructs LF functions
+% principal reductions
+βfwd : (pcomp A (\x. fwd x Y) P)
+     ⇛ (P Y).
+β1⊥  : (pcomp ① (\x. close x) (\x. wait x P))
+     ⇛ P.
+β⊗⅋  : (pcomp (A ⊗ B) (\x. (out x P Q)) (\x. inp x R))
+     ⇛ (pcomp A P (\y. pcomp B Q (\x. R x y))).
+β⊕&1 : (pcomp (A ⊕ B) (\x. inl x P) (\x. choice x Q R))
+     ⇛ (pcomp A P Q).
+β⊕&2 : (pcomp (A ⊕ B) (\x. inr x P) (\x. choice x Q R))
+     ⇛ (pcomp B P R).
+
+% commuting conversions
+κ⊥  : (pcomp C (\z. wait X (P z)) R)
+    ⇛ (wait X (pcomp C P R)).
+κ⊗1 : (pcomp C (\z. out X (\y. P y z) Q) R)
+    ⇛ (out X (\y. pcomp C (\z. P y z) R) Q).
+κ⊗2 : (pcomp C (\z. out X P (\x. Q x z)) R)
+    ⇛ (out X P (\x. pcomp C (\z. Q x z) R)).
+κ⅋  : (pcomp C (\z. inp X (\x.\y. P x y z)) Q)
+    ⇛ (inp X (\x.\y. pcomp C (\z. P x y z) Q)).
+κ⊕1 : (pcomp C (\z. inl X (\x. P x z)) Q)
+    ⇛ (inl X (\x. pcomp C (\z. P x z) Q)).
+κ⊕2 : (pcomp C (\z. inr X (\x. P x z)) Q)
+    ⇛ (inr X (\x. pcomp C (\z. P x z) Q)).
+κ&  : (pcomp C (\z. choice X (\x. P x z) (\x. Q x z)) R)
+    ⇛ (choice X (\x. pcomp C (\z. (P x z)) R) (\x. pcomp C (\z. Q x z) R)).
+
+% reduction under cut
+β∥1 : ({x:name} ((P x) ⇛ (P' x)))
+    → (pcomp A P Q) ⇛ (pcomp A P' Q).
+β∥2 : ({x:name}((Q x) ⇛ (Q' x)))
+    → (pcomp A P Q) ⇛ (pcomp A P Q').
+
+% Reductions commute with equivalences
+β≡: (P ≡ Q) → (Q ⇛ R) → (R ≡ S) → P ⇛ S.
+
diff --git a/case-studies/classical-processes/cp_lemmas.bel b/case-studies/classical-processes/cp_lemmas.bel
new file mode 100644
index 000000000..c5cf976f6
--- /dev/null
+++ b/case-studies/classical-processes/cp_lemmas.bel
@@ -0,0 +1,302 @@
+schema nctx = name;
+schema ctx = some [A:tp] block x : name, h : hyp x A;
+
+rec dual_sym : [ ⊢ dual A A' ] → [ ⊢ dual A' A] =
+/ total 1 /
+fn d ⇒
+case d of
+| [ ⊢ D1] ⇒ [ ⊢ D⊥]
+| [ ⊢ D⊥] ⇒ [ ⊢ D1]
+| [ ⊢ D⊗ Dl Dr] ⇒
+  let [ ⊢ l] = dual_sym [ ⊢ Dl] in
+  let [ ⊢ r] = dual_sym [ ⊢ Dr] in
+  [ ⊢ D⅋ l r]
+| [ ⊢ D⅋ Dl Dr] ⇒
+  let [ ⊢ l] = dual_sym [ ⊢ Dl] in
+  let [ ⊢ r] = dual_sym [ ⊢ Dr] in
+  [ ⊢ D⊗ l r]
+| [ ⊢ D⊕ Dl Dr] ⇒
+  let [ ⊢ l] = dual_sym [ ⊢ Dl] in
+  let [ ⊢ r] = dual_sym [ ⊢ Dr] in
+  [ ⊢ D& l r]
+| [ ⊢ D& Dl Dr] ⇒
+  let [ ⊢ l] = dual_sym [ ⊢ Dl] in
+  let [ ⊢ r] = dual_sym [ ⊢ Dr] in
+  [ ⊢ D⊕ l r]
+;
+
+
+rec dual_uniq : [ ⊢ dual A A' ] → [ ⊢ dual A A''] → [ ⊢ eq A' A''] =
+/ total 1 /
+fn d1 ⇒ fn d2 ⇒ case d1 of
+| [ ⊢ D1] ⇒
+  let [ ⊢ D1] = d2 in
+  [ ⊢ refl]
+| [ ⊢ D⊥] ⇒
+  let [ ⊢ D⊥] = d2 in
+  [ ⊢ refl]
+| [ ⊢ D⊗ d1l d1r] ⇒
+  let [ ⊢ D⊗ d2l d2r] = d2 in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1l] [ ⊢ d2l] in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1r] [ ⊢ d2r] in
+  [ ⊢ refl]
+| [ ⊢ D⅋ d1l d1r] ⇒
+  let [ ⊢ D⅋ d2l d2r] = d2 in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1l] [ ⊢ d2l] in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1r] [ ⊢ d2r] in
+  [ ⊢ refl]
+| [ ⊢ D& d1l d1r] ⇒
+  let [ ⊢ D& d2l d2r] = d2 in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1l] [ ⊢ d2l] in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1r] [ ⊢ d2r] in
+  [ ⊢ refl]
+| [ ⊢ D⊕ d1l d1r] ⇒
+  let [ ⊢ D⊕ d2l d2r] = d2 in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1l] [ ⊢ d2l] in
+  let [ ⊢ refl] = dual_uniq [ ⊢ d1r] [ ⊢ d2r] in
+  [ ⊢ refl]
+;
+
+% Encode contradiction with a type with no constructor %
+imposs : type.
+
+% Mechanization of "if lin(x, P) and x is not a free name in P, then contradiction"
+rec lin_name_must_appear : (g : nctx) [g ⊢ linear (\x. P[..])] → [ ⊢ imposs] =
+/ total 1 /
+fn linP ⇒ case linP of
+% principal cases are inferred to be impossible
+| [g ⊢ l_wait2 linQ] ⇒ lin_name_must_appear [g ⊢ linQ]
+| [g ⊢ l_out2 (\y. linQ)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ]
+| [g ⊢ l_out3 (\y. linQ)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ]
+| [g ⊢ l_inp2 (\y.\z. linQ)] ⇒ lin_name_must_appear [g, y:name, z:name ⊢ linQ]
+| [g ⊢ l_pcomp1 (\y. linQ)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ]
+| [g ⊢ l_pcomp2 (\y. linQ)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ]
+| [g ⊢ l_inl2 (\y. linQ)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ]
+| [g ⊢ l_inr2 (\y. linQ)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ]
+% only need to show one branch doesn't work, so just pick left branch
+| [g ⊢ l_choice2 (\y. linQ1) (\y. linQ2)] ⇒ lin_name_must_appear [g, y:name ⊢ linQ1]
+;
+
+% encode existentials for strengthening in reductions
+inductive Result : (g : ctx){P : [g ⊢ proc]}{Q : [g, x:name ⊢ proc]} → ctype =
+| Res : {Q' : [g ⊢ proc]}
+      → [g, x:name ⊢ eq_proc Q Q'[..]]
+      → [g ⊢ P ⇛ Q']
+      → Result [g ⊢ P] [g, x:name ⊢ Q]
+;
+
+% encode existentials for strengthening in equivalences
+inductive Result' : (g : ctx){P : [g ⊢ proc]}{Q : [g, x:name ⊢ proc]} → ctype =
+| Res' : {Q' : [g ⊢ proc]}
+       → [g, x:name ⊢ eq_proc Q Q'[..]]
+       → [g ⊢ P ≡ Q']
+       → Result' [g ⊢ P] [g, x:name ⊢ Q]
+;
+
+
+% strengthening on hyps -- can remove informations about types when executing reductions
+rec str_step' : (g : ctx) [g, x:name, h:hyp x A[] ⊢ P[..,x] ⇛ Q[..,x]]
+                        → [g, x:name ⊢ P ⇛ Q] =
+/ total 1 /
+fn sPP ⇒ case sPP of
+| [g, x:name, h:hyp x A[] ⊢ βfwd] ⇒ [g, x:name ⊢ βfwd]
+| [g, x:name, h:hyp x A[] ⊢ β1⊥] ⇒ [g, x:name ⊢ β1⊥]
+| [g, x:name, h:hyp x A[] ⊢ β⊗⅋] ⇒ [g, x:name |- β⊗⅋]
+| [g, x:name, h:hyp x A[] ⊢ β⊕&1] ⇒ [g, x:name |- β⊕&1]
+| [g, x:name, h:hyp x A[] ⊢ β⊕&2] ⇒ [g, x:name |- β⊕&2]
+| [g, x:name, h:hyp x A[] ⊢ κ⊥] ⇒ [g, x:name |- κ⊥]
+| [g, x:name, h:hyp x A[] ⊢ κ⊗1] ⇒ [g, x:name |- κ⊗1]
+| [g, x:name, h:hyp x A[] ⊢ κ⊗2] ⇒ [g, x:name |- κ⊗2]
+| [g, x:name, h:hyp x A[] ⊢ κ⅋] ⇒ [g, x:name |- κ⅋]
+| [g, x:name, h:hyp x A[] ⊢ κ⊕1] ⇒ [g, x:name |- κ⊕1]
+| [g, x:name, h:hyp x A[] ⊢ κ⊕2] ⇒ [g, x:name |- κ⊕2]
+| [g, x:name, h:hyp x A[] ⊢ κ&] ⇒ [g, x:name |- κ&]
+| [g, x:name, h:hyp x A[] ⊢ β∥1 (\y. sP1[..,y,x,h])] ⇒
+  let [g, bly:block (x:name, h:hyp x ⊥), x:name ⊢ sP1'[..,bly.x,x]]
+    = str_step' [g, bly:block (x:name, h:hyp x ⊥), x:name, h:hyp x A[] ⊢ sP1[..,bly.x,x,h]] in
+  [g, x:name ⊢ β∥1 (\y. sP1'[..,y,x])]
+| [g, x:name, h:hyp x A[] ⊢ β∥2 (\y. sP2[..,y,x,h])] ⇒
+  let [g, bly:block (x:name, h:hyp x ⊥), x:name ⊢ sP2'[..,bly.x,x]]
+    = str_step' [g, bly:block (x:name, h:hyp x ⊥), x:name, h:hyp x A[] ⊢ sP2[..,bly.x,x,h]] in
+  [g, x:name ⊢ β∥2 (\y. sP2'[..,y,x])]
+| [g, x:name, h:hyp x A[] ⊢ β≡ ≡PQ ⇛QR ≡RS] ⇒
+  let [g, x:name ⊢ ≡PQ'] = str_equiv' [g, x:name, h:hyp x A[] ⊢ ≡PQ] in
+  let [g, x:name ⊢ ⇛QR'] = str_step' [g, x:name, h:hyp x A[] ⊢ ⇛QR] in
+  let [g, x:name ⊢ ≡RS'] = str_equiv' [g, x:name, h:hyp x A[] ⊢ ≡RS] in
+  [g, x:name ⊢ β≡ ≡PQ' ⇛QR' ≡RS']
+and rec str_equiv' : (g : ctx) [g, x:name, h:hyp x A[] ⊢ P[..,x] ≡ Q[..,x]]
+                            → [g, x:name ⊢ P ≡ Q] =
+/ total 1 /
+fn ePP ⇒ case ePP of
+| [g, x:name, h:hyp x A[] ⊢ ≡comm D[]] ⇒ [g, x:name ⊢ ≡comm D[]]
+| [g, x:name, h:hyp x A[] ⊢ ≡assoc] ⇒ [g, x:name ⊢ ≡assoc]
+;
+
+% Strengthening of reductions
+% If P steps to Q and x does not appear in Q, then there exists a process
+% Q' where x provably does not appear such that Q = Q' and P steps to Q'
+rec str_step : (g : ctx) [g, x:name ⊢ P[..] ⇛ Q] → Result [g ⊢ P] [g, x:name ⊢ Q] =
+/ total 1 /
+fn sPP' ⇒ case sPP' of
+| [g, x:name ⊢ βfwd] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ βfwd]
+| [g, x:name ⊢ β1⊥] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β1⊥]
+| [g, x:name ⊢ β⊗⅋] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β⊗⅋]
+| [g, x:name ⊢ β⊕&1] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β⊕&1]
+| [g, x:name ⊢ β⊕&2] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β⊕&2]
+| [g, x:name ⊢ κ⊥] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ⊥]
+| [g, x:name ⊢ κ⊗1] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ⊗1]
+| [g, x:name ⊢ κ⊗2] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ⊗2]
+| [g, x:name ⊢ κ⅋] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ⅋]
+| [g, x:name ⊢ κ⊕1] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ⊕1]
+| [g, x:name ⊢ κ⊕2] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ⊕2]
+| [g, x:name ⊢ κ&] ⇒ Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ κ&]
+| [g, x:name ⊢ β∥1 (\y. s_P1[..,y,x])] ⇒
+  let Res [g, bly:block (x:name, h:hyp x ⊥)  ⊢ Q'[..,bly.x]]
+          [g, bly:block (x:name, h:hyp x ⊥), x:name ⊢ refl_proc]
+          [g, bly:block (x:name, h:hyp x ⊥) ⊢ s_P1']
+    = str_step [g, bly:block(x:name, h:hyp x ⊥), x:name ⊢ s_P1[..,bly.x,x]] in
+  let [g, y:name ⊢ s_P1''] = str_step' [g, y:name, hy:hyp y ⊥ ⊢ s_P1'[..,<y;hy>]] in
+  Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β∥1 (\y. s_P1''[..,y])]
+| [g, x:name ⊢ β∥2 (\y. s_P2[..,y,x])] ⇒
+  let Res [g, bly:block (x:name, h:hyp x ⊥)  ⊢ Q'[..,bly.x]]
+          [g, bly:block (x:name, h:hyp x ⊥), x:name ⊢ refl_proc]
+          [g, bly:block (x:name, h:hyp x ⊥) ⊢ s_P2']
+    = str_step [g, bly:block(x:name, h:hyp x ⊥), x:name ⊢ s_P2[..,bly.x,x]] in
+  let [g, y:name ⊢ s_P2''] = str_step' [g, y:name, hy:hyp y ⊥ ⊢ s_P2'[..,<y;hy>]] in
+  Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β∥2 (\y. s_P2''[..,y])]
+| [g, x:name ⊢ β≡ ≡PQ ⇛QR ≡RS] ⇒
+  let Res' [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ ≡PQ'] = str_equiv [g, x:name ⊢ ≡PQ] in
+  let Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ ⇛QR'] = str_step [g, x:name ⊢ ⇛QR] in
+  let Res' [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ ≡RS'] = str_equiv [g, x:name ⊢ ≡RS] in
+  Res [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ β≡ ≡PQ' ⇛QR' ≡RS']
+and rec str_equiv : (g : ctx) [g, x:name ⊢ P[..] ≡ Q] → Result' [g ⊢ P] [g, x:name ⊢ Q] =
+/ total 1 /
+fn ePP' ⇒ case ePP' of
+| [g, x:name ⊢ ≡comm D[]] ⇒ Res' [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ ≡comm D[]]
+| [g, x:name ⊢ ≡assoc] ⇒ Res' [g ⊢ _] [g, x:name ⊢ refl_proc] [g ⊢ ≡assoc]
+;
+
+rec str_hyp : (g:ctx) [g, z:name, hz:hyp z C[] ⊢ hyp X[..] A[]]
+                    → [g ⊢ hyp X A[]] =
+/ total (str_hyp h) /
+fn h ⇒ let [g, z:name, hz: hyp z C[] ⊢ H[..]] = h in [g ⊢ H]
+;
+
+rec str_lin : (g : nctx) [g, x:name ⊢ linear \y. P[.., y]]
+                      → [g ⊢ linear \y. P] =
+/ total 1 /
+fn linP ⇒ case linP of
+| [g, x:name ⊢ l_fwd] ⇒
+  [g ⊢ l_fwd]
+| [g, x:name ⊢ l_fwd2] ⇒
+  [g ⊢ l_fwd2]
+| [g, x:name ⊢ l_close] ⇒
+  [g ⊢ l_close]
+| [g, x:name ⊢ l_wait] ⇒
+  [g ⊢ l_wait]
+| [g, x:name ⊢ l_out linQ] ⇒
+  let [g ⊢ linQ'] = str_lin [g, x:name ⊢ linQ] in
+  [g ⊢ l_out linQ']
+| [g, x:name ⊢ l_inp (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_inp (\y. linQ')]
+| [g, x:name ⊢ l_inl linQ] ⇒
+  let [g ⊢ linQ'] = str_lin [g, x:name ⊢ linQ] in
+  [g ⊢ l_inl linQ']
+| [g, x:name ⊢ l_inr linQ] ⇒
+  let [g ⊢ linQ'] = str_lin [g, x:name ⊢ linQ] in
+  [g ⊢ l_inr linQ']
+| [g, x:name ⊢ l_choice linQ1 linQ2] ⇒
+  let [g ⊢ linQ1'] = str_lin [g, x:name ⊢ linQ1] in
+  let [g ⊢ linQ2'] = str_lin [g, x:name ⊢ linQ2] in
+  [g ⊢ l_choice linQ1' linQ2']
+| [g, x:name ⊢ l_wait2 linQ] ⇒
+  let [g ⊢ linQ'] = str_lin [g, x:name ⊢ linQ] in
+  [g ⊢ l_wait2 linQ']
+| [g, x:name ⊢ l_out2 (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_out2 (\y. linQ')]
+| [g, x:name ⊢ l_out3 (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_out3 (\y. linQ')]
+| [g, x:name ⊢ l_inp2 (\y.\z. linQ[..,y,z,x])] ⇒
+  let [g, y:name, z:name ⊢ linQ'] = str_lin [g, y:name, z:name, x:name ⊢ linQ] in
+  [g ⊢ l_inp2 (\y.\z. linQ')]
+| [g, x:name ⊢ l_pcomp1 (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_pcomp1 (\y. linQ')]
+| [g, x:name ⊢ l_pcomp2 (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_pcomp2 (\y. linQ')]
+| [g, x:name ⊢ l_inl2 (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_inl2 (\y. linQ')]
+| [g, x:name ⊢ l_inr2 (\y. linQ[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ'] = str_lin [g, y:name, x:name ⊢ linQ] in
+  [g ⊢ l_inr2 (\y. linQ')]
+| [g, x:name ⊢ l_choice2 (\y. linQ1[..,y,x]) (\y. linQ2[..,y,x])] ⇒
+  let [g, y:name ⊢ linQ1'] = str_lin [g, y:name, x:name ⊢ linQ1] in
+  let [g, y:name ⊢ linQ2'] = str_lin [g, y:name, x:name ⊢ linQ2] in
+  [g ⊢ l_choice2 (\y. linQ1') (\y. linQ2')]
+;
+
+
+%% strengthening for wtp
+rec str_wtp : (g : ctx) [g, z:name, h:hyp z C[] ⊢ wtp P[..]]
+                     → [g ⊢ wtp P] =
+/ total 1 /
+fn tpP ⇒ case tpP of
+| [g, z:name, hz:hyp z C[] ⊢ wtp_fwd D[] #bx.x[..] #bx.h[..] #bly.x[..] #bly.h[..]] ⇒
+  [g ⊢ wtp_fwd D[] #bx.x #bx.h #bly.x #bly.h]
+| [g, z:name, hz:hyp z C[] ⊢ wtp_close #bx.x[..] #bx.h[..]] ⇒
+  [g ⊢ wtp_close #bx.x #bx.h]
+| [g, z:name, hz:hyp z C[] ⊢ wtp_wait #bx.x[..] #bx.h[..] wtpP'] ⇒
+  let [g ⊢ wtpP''] = str_wtp [g, z:name, hz:hyp z C[] ⊢ wtpP'] in
+  [g ⊢ wtp_wait #bx.x #bx.h wtpP'']
+| [g, z:name, hz:hyp z C[] ⊢ wtp_out linP1[..,z] x[..] hx
+    (\y.\hy.wtpP1[..,y,hy,z,hz]) (\x'.\hx'.wtpP2[..,x',hx',z,hz])] ⇒
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z C[]  ⊢ hx] in
+  let [g, bly:block x:name, h:hyp x _ ⊢ wtpP1'[..,bly.x,bly.h]] =
+    str_wtp [g, bly:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpP1[..,bly.x,bly.h,z,hz]] in
+  let [g, bx':block x:name, h:hyp x _ ⊢ wtpP2'[..,bx'.x,bx'.h]] =
+    str_wtp [g, bx':block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpP2[..,bx'.x,bx'.h,z,hz]] in
+  let [g ⊢ linP1'] = str_lin [g, z:name ⊢ linP1] in
+  [g ⊢ wtp_out linP1' x hx' (\y.\hy.wtpP1') (\x'.\hx'.wtpP2')]
+| [g, z:name, hz:hyp z C[] ⊢ wtp_inp (\x.linP'[..,x,z]) x[..] hx
+                                      (\x'.\hx'.\y.\hy.wtpP'[..,x',hx',y,hy,z,hz])] ⇒
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z C[]  ⊢ hx] in
+  let [g, bx':block (x:name, h:hyp x _), bly:block (x:name, h:hyp x _)
+    ⊢ wtpP''[..,bx'.x,bx'.h,bly.x,bly.h]] =
+    str_wtp [g, bx':block (x:name, h:hyp x _), bly:block (x:name, h:hyp x _), z:name, hz:hyp z C[]
+    ⊢ wtpP'[..,bx'.x,bx'.h,bly.x,bly.h,z,hz]] in
+  let [g, x:name ⊢ linP''] = str_lin [g, x:name, z:name ⊢ linP'] in
+  [g ⊢ wtp_inp (\x.linP'') x hx' (\x'.\hx'.\y.\hy.wtpP'')]
+| [g, z:name, hz:hyp z C[] ⊢ wtp_pcomp D[] (\x. \hx. wtpP[..,x,hx,z,hz])
+                                           (\x. \hx. wtpQ[..,x,hx,z,hz])
+                                           linP[..,z] linQ[..,z]] ⇒
+  let [g, bx:block x:name, h:hyp x _ ⊢ wtpP'[..,bx.x, bx.h]] =
+    str_wtp [g, bx:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpP[..,bx.x,bx.h,z,hz]] in
+  let [g, bx:block x:name, h:hyp x _ ⊢ wtpQ'[..,bx.x, bx.h]] =
+    str_wtp [g, bx:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpQ[..,bx.x,bx.h,z,hz]] in
+  let [g ⊢ linP'] = str_lin [g, z:name ⊢ linP] in
+  let [g ⊢ linQ'] = str_lin [g, z:name ⊢ linQ] in
+  [g ⊢ wtp_pcomp D[] (\x.\hx.wtpP') (\x.\hx.wtpQ') linP' linQ']
+| [g, z:name, hz:hyp z C[] ⊢ wtp_inl x[..] hx (\x'.\hx'.wtpP'[..,x',hx',z,hz])] ⇒
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z C[]  ⊢ hx] in
+  let [g, bx:block x:name, h:hyp x _ ⊢ wtpP''[..,bx.x, bx.h]] =
+    str_wtp [g, bx:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpP'[.., bx.x,bx.h, z, hz]] in
+  [g ⊢ wtp_inl x hx' (\x'.\hx'.wtpP'')]
+| [g, z:name, hz:hyp z C[] ⊢ wtp_inr x[..] hx (\x'.\hx'.wtpP'[..,x',hx',z,hz])] ⇒
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z C[]  ⊢ hx] in
+  let [g, bx:block x:name, h:hyp x _ ⊢ wtpP''[..,bx.x, bx.h]] =
+    str_wtp [g, bx:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpP'[.., bx.x,bx.h, z, hz]] in
+  [g ⊢ wtp_inr x hx' (\x'.\hx'.wtpP'')]
+| [g, z:name, hz:hyp z C[] ⊢ wtp_choice x[..] hx (\x'. \hx'. wtpP[..,x',hx', z, hz]) (\x'. \hx'. wtpQ[..,x',hx',z, hz])] ⇒
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z C[]  ⊢ hx] in
+  let [g, bx:block x:name, h:hyp x _ ⊢ wtpP'[..,bx.x, bx.h]] =
+    str_wtp [g, bx:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpP[.., bx.x,bx.h, z, hz]] in
+  let [g, bx:block x:name, h:hyp x _ ⊢ wtpQ'[..,bx.x, bx.h]] =
+    str_wtp [g, bx:block (x:name, h:hyp x _), z:name, hz:hyp z C[] ⊢ wtpQ[..,bx.x,bx.h,z, hz]] in
+  [g ⊢  wtp_choice x hx' (\x'. \hx'. wtpP') (\x'. \hx'. wtpQ')]
+;
+
diff --git a/case-studies/classical-processes/cp_linear.bel b/case-studies/classical-processes/cp_linear.bel
new file mode 100644
index 000000000..dee225d5f
--- /dev/null
+++ b/case-studies/classical-processes/cp_linear.bel
@@ -0,0 +1,49 @@
+% linearity predicate: check that name occurs linearly in proc
+linear: (name → proc) → type.
+
+% Most constructs (except close and cut) have a "principle" case, where the abstracted channel is being used in the
+% process, and some "congruence" cases, where the abstracted channel is not immediately being used and therefore need to
+% be passed.
+
+% principle cases: Aside from close and wait, where the channel continuation does not exist, all other cases require
+% that the appropriate continuation process are themselves linear in the "new" channel
+
+% axioms
+l_fwd   : linear (\x. fwd x Y).
+l_fwd2  : linear (\x. fwd Y x).
+l_close : linear (\x. close x).
+l_wait  : linear (\x. wait x P).
+
+l_out   : linear Q → linear (\x. out x P Q).
+l_inp   : ({y:name} linear (\x. P x y)) →  linear (\x. inp x P).
+l_inl   : linear P → linear (\x. inl x P).
+l_inr   : linear P → linear (\x. inr x P).
+l_choice: linear P → linear Q → linear (\x. choice x P Q).
+
+% congruence cases
+
+% note that pcomp only has congruence
+l_pcomp1: ({x:name}linear  (\z. P x z))
+        → linear  (\z. pcomp A (\x. P x z)  Q).
+l_pcomp2: ({x:name}linear  (\z. Q x z))
+        → linear  (\z. pcomp A P (\x. Q x z)).
+
+% (no congruence case for close)
+l_wait2: linear P → linear (\z. wait X (P z)).
+
+% z can appear in either the P or Q, so we need two congruence rules for out
+l_out2 : ({y:name} linear (\z. P z y))
+       → linear (\z. out X (P z) Q).
+l_out3 : ({x':name}linear (\z. Q z x'))
+       → linear (\z. out X P (Q z)).
+l_inp2 : ({x:name}{y:name} linear (\z. P z x y))
+       → linear (\z. inp X (P z)).
+
+
+l_inl2   : ({x':name}linear (\z. P z x')) → linear (\z. inl X (P z)).
+l_inr2   : ({x':name}linear (\z. P z x')) → linear (\z. inr X (P z)).
+% case is additive, so z must appear linearly in both branches
+l_choice2: ({x':name}linear (\z. P z x'))
+         → ({x':name}linear (\z. Q z x'))
+         → linear (\z. choice X (P z) (Q z)).
+
diff --git a/case-studies/classical-processes/cp_statics.bel b/case-studies/classical-processes/cp_statics.bel
new file mode 100644
index 000000000..703e84d8b
--- /dev/null
+++ b/case-studies/classical-processes/cp_statics.bel
@@ -0,0 +1,47 @@
+% Typing -- with linearity enforced.
+% Linearity is introduced every time a fresh channel is being bound to some process. Linearity of continuation channels
+% (which technically can be interpreted as fresh) are checked already inside the linearity predicate, so we only need to
+% introduce linearity conditions for when a fresh channel is being made on paper.
+
+% Hypothesis -- encodes typing assumptions of form x:A
+hyp : name → tp → type.
+% wtp P means that P is well-typed with respect to some context
+wtp : proc → type.
+
+wtp_fwd   : dual A A'
+          → {X:name}hyp X A → {Y:name}hyp Y A'
+          → wtp (fwd X Y).
+wtp_pcomp :  dual A A'
+          → ({x:name} hyp x A → wtp (P x))
+          → ({x:name} hyp x A' → wtp (Q x))
+          → linear P
+          → linear Q
+          → wtp (pcomp A P Q).
+
+wtp_close : {X:name}hyp X one
+          → wtp (close X).
+wtp_wait  : {X:name}hyp X bot
+          → wtp P
+          → wtp (wait X P).
+
+wtp_out   : linear P % y is fresh and being bound to P, so check that it's linear
+          → {X:name}hyp X (A ⊗ B)
+	  → ({y:name}hyp y A → wtp (P y))
+	  → ({x:name}hyp x B → wtp (Q x))
+	  → wtp (out X P Q).
+wtp_inp   : ({x:name}linear (P x)) % check linearity for the input channel y
+          → {X:name}hyp X (A ⅋ B)
+          → ({x:name}hyp x B → {y:name}hyp y A → wtp (P x y))
+          → wtp (inp X P).
+
+wtp_inl   : {X:name}hyp X (A ⊕ B)
+          → ({x:name}hyp x A → wtp (P x))
+          → wtp (inl X P).
+wtp_inr   : {X:name}hyp X (A ⊕ B)
+          → ({x:name}hyp x B → wtp (P x))
+          → wtp (inr X P).
+wtp_choice: {X:name}hyp X (A & B)
+             → ({x:name}hyp x A → wtp (P x))
+             → ({x:name}hyp x B → wtp (Q x))
+             → wtp (choice X P Q).
+
diff --git a/case-studies/classical-processes/cp_thrm.bel b/case-studies/classical-processes/cp_thrm.bel
new file mode 100644
index 000000000..ca035068a
--- /dev/null
+++ b/case-studies/classical-processes/cp_thrm.bel
@@ -0,0 +1,390 @@
+% Linearity is preserved under structural equivalences
+rec lin_s≡ : (g : ctx) [g, x:name ⊢ P[..,x] ≡ P'[..,x] ]
+                     → [g ⊢ linear (\x. P)]
+                     → [g ⊢ linear (\x. P')] =
+/ total 1 /
+fn ePP' ⇒ fn lP ⇒ case ePP' of
+| [g, x:name ⊢ ≡comm _] ⇒
+  (case lP of
+  | [g ⊢ l_pcomp1 (\y. linP')] ⇒ [g ⊢ l_pcomp2 (\y. linP')]
+  | [g ⊢ l_pcomp2 (\y. linP')] ⇒ [g ⊢ l_pcomp1 (\y. linP')]
+  )
+| [g, x:name ⊢ ≡assoc] ⇒
+  (case lP of
+  | [g ⊢ l_pcomp1 (\y. l_pcomp1 (\x. linP[..,x,y]))] ⇒
+    let [g, x:name ⊢ linP'] = str_lin [g, x:name, y:name ⊢ linP] in
+    [g ⊢ l_pcomp1 (\x. linP')]
+  | [g ⊢ l_pcomp1 (\y. l_pcomp2 (\x. linQ))] ⇒
+    [g ⊢ l_pcomp2 (\x. l_pcomp1 (\y. linQ[..,y,x]))]
+  | [g ⊢ l_pcomp2 (\y. linR)] ⇒
+    [g ⊢ l_pcomp2 (\x. l_pcomp2 (\y. linR[..,y]))]
+  )
+;
+
+% Typing is preserved under structural equivalences
+rec wtp_s≡ : (g : ctx) [g ⊢ wtp P ] → [g ⊢ P ≡ P' ] → [g ⊢ wtp P' ] =
+/ total 1 /
+fn tpP ⇒ fn ePP' ⇒ case ePP' of
+| [g ⊢ ≡comm D[]] ⇒
+  let [g ⊢ wtp_pcomp D'[] (\x.\h. wtp_P) (\x.\h. wtp_Q) linP linQ] = tpP in
+  let [ ⊢ refl]  = dual_uniq [⊢ D] [⊢ D'] in
+  let [ ⊢ D''] = dual_sym [ ⊢ D] in
+  [g ⊢ wtp_pcomp D''[] (\x.\h. wtp_Q) (\x.\h. wtp_P) linQ linP]
+| [g ⊢ ≡assoc] ⇒
+  let [g ⊢ wtp_pcomp D'[] (\y.\hy. wtpPQ) (\y.\hy. wtpR) linPQy linRy] = tpP in
+  let [g, y:name, hy:hyp y _ ⊢ wtp_pcomp D[]
+      (\x.\hx. wtpP[..,x,hx,y,hy]) (\x.\hx. wtpQ) linPx[..,y] linQx[..,y]]
+    = [g, y:name, hy:hyp y _ ⊢ wtpPQ] in
+  let [g, blx:block(x:name, h:hyp x _) ⊢ wtpP']
+    = str_wtp [g, blx:block(x:name, h:hyp x _), y:name, hy:hyp y _
+               ⊢ wtpP[..,blx.x,blx.h,y,hy]] in
+  let [g ⊢ linPx'] = str_lin [g, y:name ⊢ linPx] in
+  (case [g ⊢ linPQy] of
+  | [g ⊢ l_pcomp1 (\y. linPy)] ⇒
+    impossible lin_name_must_appear [g, y:name ⊢ linPy]
+  | [g ⊢ l_pcomp2 (\y. linQy)] ⇒
+    [g ⊢ wtp_pcomp D[]
+      (\x.\hx. wtpP'[..,<x;hx>])
+      (\x.\hx. wtp_pcomp D'[] (\y.\hy. wtpQ[..,y,hy,x,hx]) (\y.\hy. wtpR[..,y,hy])
+               linQy[..,x] linRy[..])
+      linPx' (l_pcomp1 (\y. linQx))]
+  )
+;
+
+
+%% subject reduction for linear
+rec lin_s : (g : ctx) [g, x:name, h:hyp x A[] ⊢ wtp P[..,x] ]
+                   → [g, x:name ⊢ P[..,x] ⇛ P'[..,x] ]
+                   → [g ⊢ linear (\x. P)]
+                   → [g ⊢ linear (\x. P')] =
+/ total 2 /
+fn tpP ⇒ fn sPP' ⇒ fn linP ⇒
+case sPP' of
+| [g, x:name ⊢ βfwd] ⇒
+  let [g, x:name, h:hyp x A[] ⊢
+    wtp_pcomp D[] (\x'.\h'. tpP')
+                  (\x'.\h'.tpQ)
+                  linP''[..,x] linQ[..,x]] = tpP in
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_fwd2)] ⇒
+    str_lin [g, x:name ⊢ linQ]
+  | [g ⊢ l_pcomp2 (\x. linQ')] ⇒
+    let [g, x:name, h: hyp x A[], x':name, h':hyp x' _ ⊢
+      wtp_fwd D'[] x' h' y[..] _ ] =
+    [g, x:name, h: hyp x A[], x':name, h':hyp x' _ ⊢ tpP'] in
+    [g ⊢ linQ'[..,y]]
+  )
+| [g, x:name ⊢ β⊗⅋] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. (l_out2 \y.linP1))] ⇒
+    [g ⊢ l_pcomp1 (\y. linP1[.., y])]
+  | [g ⊢ l_pcomp1 (\x. (l_out3 (\x'. linP2)))] ⇒
+    [g ⊢ l_pcomp2 (\y. (l_pcomp1 (\x. linP2[..,x,x])))]
+  | [g ⊢ l_pcomp2 (\x. (l_inp2 \x'.\y. linQ))] ⇒
+    [g ⊢ l_pcomp2 (\y. (l_pcomp2 (\x. linQ[..,x,x,y])))]
+  )
+| [g, x:name ⊢ β⊕&1] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_inl2 (\x'.linP'))] ⇒
+    [g ⊢ l_pcomp1 (\x. linP'[..,x,x])]
+  | [g ⊢ l_pcomp2 (\x. l_choice2 (\x'. linQl) (\x'._))] ⇒
+    [g ⊢ l_pcomp2 (\x. linQl[..,x,x])]
+  )
+| [g, x:name ⊢ β⊕&2] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_inr2 (\x'.linP'))] ⇒
+    [g ⊢ l_pcomp1 (\x. linP'[..,x,x])]
+  | [g ⊢ l_pcomp2 (\x. l_choice2 (\x'._) (\x'.linQr))] ⇒
+    [g ⊢ l_pcomp2 (\x. linQr[..,x,x])]
+  )
+| [g, x:name ⊢ β1⊥] ⇒
+  let [g ⊢ l_pcomp2 (\x. l_wait2 linP')] = linP in
+  str_lin [g, x:name ⊢ linP']
+ %commuting conversions
+| [g, x:name ⊢ κ⊥] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_wait)] ⇒
+    [g ⊢ l_wait]
+  | [g ⊢ l_pcomp1 (\x. l_wait2 linP')] ⇒
+    [g ⊢ l_wait2 (l_pcomp1 (\x. linP'))]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_wait2 (l_pcomp2 (\x. linQ))]
+  )
+| [g, x:name  ⊢ κ⊗1] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_out linP2)] ⇒
+    str_lin [g, x:name ⊢ l_out linP2]
+  | [g ⊢ l_pcomp1 (\x. (l_out2 \y. linP1))] ⇒
+    [g ⊢ l_out2 (\y. l_pcomp1 (\x. linP1[..,x,y]))]
+  | [g ⊢ l_pcomp1 (\x. (l_out3 \x'. linP2))] ⇒
+    str_lin [g, x:name ⊢ l_out3 \x'. linP2]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_out2 (\y. l_pcomp2 (\x. linQ[..,x]))]
+  )
+| [g,  x:name ⊢ κ⊗2] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_out linP2)] ⇒
+    [g ⊢ l_out (l_pcomp1 (\x. linP2))]
+  | [g ⊢ l_pcomp1 (\x. (l_out2 \y. linP1))] ⇒
+    str_lin [g, x:name ⊢ l_out2 (\y. linP1)]
+  | [g ⊢ l_pcomp1 (\x. (l_out3 \x'. linP2))] ⇒
+    [g ⊢ l_out3 \x'.(l_pcomp1 (\x. linP2[..,x,x']))]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_out3 \x'. (l_pcomp2 (\x. linQ[..,x]))]
+  )
+| [g, x:name ⊢ κ⅋] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_inp (\y. linP'))] ⇒
+    [g ⊢ l_inp (\y. l_pcomp1 (\x. linP'[..,x,y]))]
+  | [g ⊢ l_pcomp1 (\x. (l_inp2 \x'. \y. linP'))] ⇒
+    [g ⊢ l_inp2 (\x'. \y. l_pcomp1 (\x. linP'[..,x,x',y]))]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_inp2 (\x'. \y. l_pcomp2 (\x. linQ[..,x]))]
+  )
+| [g,  x:name ⊢ κ⊕1] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_inl linP')] ⇒
+    [g ⊢ l_inl (l_pcomp1 (\x. linP'))]
+  | [g ⊢ l_pcomp1 (\x. (l_inl2 \x'. linP'))] ⇒
+    [g ⊢ l_inl2 \x'. (l_pcomp1 (\x. linP'[..,x,x']))]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_inl2 \x'. (l_pcomp2 (\x. linQ[..,x]))]
+  )
+| [g,  x:name ⊢ κ⊕2] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_inr linP')] ⇒
+    [g ⊢ l_inr (l_pcomp1 (\x. linP'))]
+  | [g ⊢ l_pcomp1 (\x. (l_inr2 \x'. linP'))] ⇒
+    [g ⊢ l_inr2 \x'. (l_pcomp1 (\x. linP'[..,x,x']))]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_inr2 \x'. (l_pcomp2 (\x. linQ[..,x]))]
+  )
+| [g, x:name ⊢ κ&] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. l_choice linP1 linP2)] ⇒
+    [g ⊢ l_choice (l_pcomp1 (\x. linP1)) (l_pcomp1 (\x. linP2))]
+  | [g ⊢ l_pcomp1 (\x. (l_choice2 (\x'. linP1) (\x'. linP2)))] ⇒
+    [g ⊢ l_choice2 (\x'. l_pcomp1 (\x. linP1[..,x,x']))
+                   (\x'. l_pcomp1 (\x. linP2[..,x,x']))]
+  | [g ⊢ l_pcomp2 (\x. linQ)] ⇒
+    [g ⊢ l_choice2 (\x'. l_pcomp2 (\x. linQ[..,x])) (\x'. l_pcomp2 (\x. linQ[..,x]))]
+  )
+| [g, x:name ⊢ β∥1 (\y. sPl[..,y,x])] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. linPl)] ⇒
+    let [g, x:name, h:hyp x A[] ⊢ wtp_pcomp D[] (\y.\hy.tpPl) (\y.\hy.tpPr) lP[..,x] lQ[..,x]] = tpP in
+    let [g, bly:block x:name, h:hyp x B[] ⊢ linPl'[..,bly.x]] =
+    lin_s [g, bly:block (x:name, h:hyp x _), x:name, h:hyp x A[] ⊢ tpPl[..,x, h,bly.x,bly.h]]
+          [g, bly:block (x:name, h:hyp x _), x:name  ⊢ sPl[..,bly.x, x]]
+          [g, bly:block (x:name, h:hyp x _) ⊢ linPl[.., bly.x]] in
+    [g ⊢ l_pcomp1 (\x. linPl')]
+  | [g ⊢ l_pcomp2 (\x. linPr)] ⇒
+    let Res [g, b:block (x:name, h:hyp x ⊥) ⊢ _]
+            [g, b:block (x:name, h:hyp x ⊥), x:name |- refl_proc]
+            [g, b:block (x:name, h:hyp x ⊥) ⊢ sPl'] =
+      str_step [g, b:block (x:name, h:hyp x ⊥), x:name ⊢ sPl[..,b.1,x]] in
+    [g ⊢ l_pcomp2 (\x. linPr)]
+  )
+
+| [g, x:name ⊢ β∥2 (\y. sPr[..,y,x])] ⇒
+  (case linP of
+  | [g ⊢ l_pcomp1 (\x. linPl)] ⇒
+    let Res [g, b:block (x:name, h:hyp x ⊥) ⊢ _]
+            [g, b:block (x:name, h:hyp x ⊥), x:name |- refl_proc]
+            [g, b:block (x:name, h:hyp x ⊥) ⊢ sPr'] =
+      str_step [g, b:block (x:name, h:hyp x ⊥), x:name ⊢ sPr[..,b.1,x]] in
+    [g ⊢ l_pcomp1 (\x. linPl)]
+  | [g ⊢ l_pcomp2 (\x. linPr)] ⇒
+    let [g, x:name, h:hyp x A[] ⊢ wtp_pcomp D[] (\y.\hy.tpPl) (\y.\hy.tpPr) lP[..,x] lQ[..,x]] = tpP in
+    let [g, bly:block x:name, h:hyp x B[] ⊢ linPr'[..,bly.x]] =
+    lin_s [g, bly:block (x:name, h:hyp x _), x:name, h:hyp x A[] ⊢ tpPr[..,x, h,bly.x,bly.h]]
+          [g, bly:block (x:name, h:hyp x _), x:name  ⊢ sPr[..,bly.x, x]]
+          [g, bly:block (x:name, h:hyp x _) ⊢ linPr[.., bly.x]] in
+    [g ⊢ l_pcomp2 (\x. linPr')]
+  )
+| [g, x:name ⊢ β≡ ≡PQ ⇛QR ≡RS] ⇒
+  let [g ⊢ linQ] = lin_s≡ [g, x:name ⊢ ≡PQ] linP in
+  let [g, x:name, h:hyp x A[] ⊢ wtpP] = tpP in
+  let [g, b:block(x:name, h:hyp x A[]) ⊢ wtpQ]
+    = wtp_s≡ [g, b:block(x:name, h:hyp x A[]) ⊢ wtpP[..,b.x,b.h]]
+             [g, b:block(x:name, h:hyp x A[]) ⊢ ≡PQ[..,b.x]] in
+  let [g ⊢ linR] = lin_s [g, x:name, h:hyp x A[] ⊢ wtpQ[..,<x;h>]]
+                         [g, x:name ⊢ ⇛QR] [g ⊢ linQ] in
+  let [g, b:block(x:name, h:hyp x A[]) ⊢ wtpR]
+    = wtp_s [g, b:block(x:name, h:hyp x A[]) ⊢ wtpQ]
+             [g, b:block(x:name, h:hyp x A[]) ⊢ ⇛QR[..,b.x]] in
+  lin_s≡ [g, x:name ⊢ ≡RS] [g ⊢ linR]
+and
+rec wtp_s : (g : ctx) [g ⊢ wtp P ] → [g ⊢ P ⇛ P' ] → [g ⊢ wtp P' ] =
+/ total 2 /
+fn tpP ⇒ fn sPP' ⇒ case sPP' of
+| [g ⊢ βfwd] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) linP linQ] = tpP in
+  let ([ ⊢ D] : [ ⊢ dual A A']) = [ ⊢ D] in
+  let [g, x:name,h:hyp x A[] ⊢ wtp_fwd D'[] x h #y.1[..] #y.2[..] ] = [_ ⊢ wtp_P] in
+  let ( [⊢ D'] : [ ⊢ dual A[] A'']) = [ ⊢ D'] in
+  let [⊢ refl]  = dual_uniq [⊢ D] [⊢ D'] in
+  [g ⊢ wtp_Q[.., #y.1, #y.2]]
+
+| [g ⊢ β⊗⅋] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) (l_out linP2) (l_inp (\x. linQx))] = tpP in
+  let ([ ⊢ D⊗ Dl Dr] : [ ⊢ dual (A ⊗ B) (A' ⅋ B')]) = [ ⊢ D] in
+  let [g, x:name,h:hyp x (A[] ⊗ B[])
+		       ⊢ wtp_out linP1[..,x] x h (\y.\hy. wtp_P1) (\x'.\h'. wtp_P2)] = [_ ⊢ wtp_P] in
+  let [g, x:name,h:hyp x (A'[] ⅋ B'[])
+		       ⊢ wtp_inp (\y. linQy[..,y,x]) x h (\x'.\h'.\y.\hy. wtp_Q')] = [_ ⊢ wtp_Q] in
+
+  let [g ⊢ linP1'] = str_lin [g, x:name ⊢ linP1] in
+  let [g, bly:block x:name, h:hyp x A[] ⊢ wtp_P1'] =
+    str_wtp [g, bly:block (x:name, h:hyp x A[]), x:name, hx:hyp x (A[] ⊗ B[]) ⊢ wtp_P1[..,x,hx,bly.x,bly.h]] in
+  let [g, blx':block (x:name, h:hyp x B[]) ⊢ wtp_P2'] =
+    str_wtp [g, blx':block (x:name, h:hyp x B[]), x:name, hx:hyp x (A[] ⊗ B[])
+      ⊢ wtp_P2[..,x,hx,blx'.x,blx'.h]] in
+  let [g, blx':block (x:name, h:hyp x B'[]), bly:block (x:name, h:hyp x A'[]) ⊢ wtp_Q''] =
+    str_wtp [g, blx':block (x:name, h:hyp x B'[]), bly:block (x:name, h:hyp x A'[]), x:name, hx:hyp x (A'[] ⅋ B'[]) ⊢ wtp_Q'[..,x,hx,blx'.x,blx'.h,bly.x,bly.h]] in
+  [g ⊢ wtp_pcomp Dl[] (\y. \hy. wtp_P1'[..,<y;hy>])
+    (\y. \hy. wtp_pcomp Dr[] (\x.\h. wtp_P2'[..,<x;h>]) (\x.\h. wtp_Q''[..,<x;h>,<y;hy>]) linP2[..] linQx[.., y])
+    linP1' (l_pcomp2 \x. linQy[..,x])]
+
+| [g ⊢ β⊕&1] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) linP linQ] = tpP in
+  let ([ ⊢ D⊕ Dl Dr] : [ ⊢ dual (A ⊕ B) (A' & B')]) = [ ⊢ D] in
+  let [g, x:name,h:hyp x (A[] ⊕ B[]) ⊢ wtp_inl x h (\x'. \h'. wtp_P')] = [_ ⊢ wtp_P] in
+  let [g, x:name,h:hyp x (A'[] & B'[]) ⊢ wtp_choice x h (\x'.\h'. wtp_Q') (\x'. \h'. _)] = [_ ⊢ wtp_Q] in
+  let [g ⊢ l_inl linP'] = [g ⊢ linP] in
+  let [g ⊢ l_choice linQ' _] = [g ⊢ linQ] in
+  let [g, blx':block (x:name, h:hyp x A[]) ⊢ wtp_P''] =
+    str_wtp [g, blx':block (x:name, h:hyp x A[]), x:name, h:hyp x (A[] ⊕ B[])
+      ⊢ wtp_P'[..,x,h,blx'.x,blx'.h]] in
+  let [g, blx':block (x:name, h:hyp x A'[]) ⊢ wtp_Q''] =
+    str_wtp [g, blx':block (x:name, h:hyp x A'[]), x:name, h:hyp x (A'[] & B'[])
+      ⊢ wtp_Q'[..,x,h,blx'.x,blx'.h]] in
+  [g ⊢ wtp_pcomp Dl[] (\x.\h. wtp_P''[..,<x;h>]) (\x. \h. wtp_Q''[..,<x;h>]) linP' linQ']
+| [g ⊢ β⊕&2] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) linP linQ] = tpP in
+  let ([ ⊢ D⊕ Dl Dr] : [ ⊢ dual (A ⊕ B) (A' & B')]) = [ ⊢ D] in
+  let [g, x:name,h:hyp x (A[] ⊕ B[]) ⊢ wtp_inr x h (\x'. \h'. wtp_P')] = [_ ⊢ wtp_P] in
+  let [g, x:name,h:hyp x (A'[] & B'[]) ⊢ wtp_choice x h (\x'.\h'._) (\x'.\h'.wtp_Q')] = [_ ⊢ wtp_Q] in
+  let [g ⊢ l_inr linP'] = [g ⊢ linP] in
+  let [g ⊢ l_choice _ linR'] = [g ⊢ linQ] in
+  let [g, blx':block (x:name, h:hyp x B[]) ⊢ wtp_P''] =
+    str_wtp [g, blx':block (x:name, h:hyp x B[]), x:name, h:hyp x (A[] ⊕ B[])
+      ⊢ wtp_P'[..,x,h,blx'.x,blx'.h]] in
+  let [g, blx':block (x:name, h:hyp x B'[]) ⊢ wtp_Q''] =
+    str_wtp [g, blx':block (x:name, h:hyp x B'[]), x:name, h:hyp x (A'[] & B'[])
+      ⊢ wtp_Q'[..,x,h,blx'.x,blx'.h]] in
+  [g ⊢ wtp_pcomp Dr[] (\x.\h. wtp_P''[..,<x;h>]) (\x.\h. wtp_Q''[..,<x;h>]) linP' linR']
+| [g ⊢ β1⊥] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) linP linQ] = tpP in
+  let ([ ⊢ D1] : [ ⊢ dual ① ⊥]) = [ ⊢ D] in
+  let [g, x:name,h:hyp x ① ⊢ wtp_close x h] = [g, x:name,h:hyp x ① ⊢ wtp_P] in
+  let [g, x:name,h:hyp x ⊥ ⊢ wtp_wait x h wtp_Q' ] = [_ ⊢ wtp_Q] in
+  str_wtp [g, x:name, h:hyp x ⊥ ⊢ wtp_Q']
+
+%  commuting conversions
+| [g ⊢ κ⊥] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z.\hz. wtp_P) (\z.\hz. wtp_Q) linP linQ] = tpP in
+  let [g,z:name, hz:hyp z _ ⊢ wtp_wait x[..] hx wtp_P']
+    = [g,z:name, hz:hyp z _ ⊢ wtp_P] in
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z _ ⊢ hx] in
+  let [g ⊢ l_wait2 linP'] = [g ⊢ linP] in
+  [g ⊢ wtp_wait x hx' (wtp_pcomp D[] (\z.\hz. wtp_P') (\z.\hz. wtp_Q) linP' linQ)]
+
+| [g ⊢ κ⊗1] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z.\hz. wtp_P) (\z.\hz. wtp_Q) linP linQ] = tpP in
+  let [g,z:name, hz:hyp z _ ⊢ wtp_out linP1[..,z] x[..] hx
+    (\y.\hy. wtpP1) (\x'.\hx'. wtpP2)] = [g,z:name, hz:hyp z _ ⊢ wtp_P] in
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z _ ⊢ hx] in
+  let [g,bly:block (x:name, h:hyp x _) ⊢ wtpP2'] =
+    str_wtp [g, blx':block (x:name, h:hyp x _), z:name, hz:hyp z _ ⊢ wtpP2[..,z,hz,blx'.x,blx'.h]] in
+  (case [g ⊢ linP] of
+  | [g ⊢ l_out2 (\y. linP')] ⇒
+    [g ⊢ wtp_out (l_pcomp1 \z. linP1) x hx'
+      (\y.\hy. wtp_pcomp D[] (\z.\hz.wtpP1[..,z,hz,y,hy]) (\z.\hz.wtp_Q[..,z,hz])
+                             linP'[..,y] linQ[..])
+      (\x'.\hx'. wtpP2'[..,<x';hx'>])]
+  | [g ⊢ l_out3 (\x'. linP')] ⇒
+    % z is a free var in P1, so it cannot occur in P2 (l_out3)
+    impossible lin_name_must_appear [g, y:name ⊢ linP']
+  )
+| [g ⊢ κ⊗2] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z.\hz. wtp_P) (\z.\hz. wtp_Q) linP linQ] = tpP in
+  let [g,z:name, hz:hyp z _ ⊢ wtp_out linP1[..,z] x[..] hx
+    (\y.\hy. wtpP1) (\x'.\hx'. wtpP2)] = [g,z:name, hz:hyp z _ ⊢ wtp_P] in
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z _ ⊢ hx] in
+  let [g ⊢ linP1'] = str_lin [g, z:name ⊢ linP1] in
+  let [g,bly:block (x:name, h:hyp x _) ⊢ wtpP1'] =
+    str_wtp [g, bly:block (x:name, h:hyp x _), z:name, hz:hyp z _ ⊢ wtpP1[..,z,hz,bly.x,bly.h]] in
+  (case [g ⊢ linP] of
+  | [g ⊢ l_out2 (\y. linP')] ⇒
+    % z is a free var in P2, so it cannot occur in P1 (l_out2)
+    impossible lin_name_must_appear [g, y:name ⊢ linP']
+  | [g ⊢ l_out3 (\x'. linP')] ⇒
+    [g ⊢ wtp_out linP1' x hx' (\y.\hy. wtpP1'[..,<y;hy>])
+      (\x'.\hx'. wtp_pcomp D[] (\z.\hz. wtpP2[..,z,hz,x',hx']) (\z.\hz.wtp_Q[..,z,hz])
+                                        linP'[..,x'] linQ[..])]
+  )
+| [g ⊢ κ⅋] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z.\hz. wtp_P) (\z.\hz. wtp_Q) (l_inp2 \x'.\y. linP') linQ] = tpP in
+  let [g,z:name, hz:hyp z _ ⊢ wtp_inp (\x. linPy[..,z,x]) x[..] hx (\x'.\hx'.\y.\hy. wtpP')] = [g,z:name, hz:hyp z _ ⊢ wtp_P] in
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z _ ⊢ hx] in
+  [g ⊢ wtp_inp (\x'. l_pcomp1 (\z. linPy[..,z,x'])) x hx'
+    (\x'.\hx'.\y.\hy. wtp_pcomp D[] (\z.\hz. wtpP'[..,z,hz,x',hx',y,hy]) (\z.\hz. wtp_Q[..,z,hz]) linP'[..,x',y] linQ[..])]
+| [g ⊢ κ⊕1] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z. \hz. wtp_P) (\z. \hz. wtp_Q) (l_inl2 \x'. linP') linQ] = tpP in
+  let ([ ⊢ D] : [ ⊢ dual A A']) = [ ⊢ D] in
+  let [g, z:name, hz:hyp z A[] ⊢ wtp_inl x[..] hx (\x'. \hx'. wtp_P'[.., x', hx', z, hz])]
+    = [g, z:name, hz:hyp z A[] ⊢ wtp_P] in
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z A[] ⊢ hx] in
+   [g ⊢ wtp_inl x hx'
+    (\x'.\h'. wtp_pcomp D[] (\z.\hz. wtp_P') (\z.\hz. wtp_Q[.., z, hz]) linP'[..,x'] linQ[..])]
+| [g ⊢ κ⊕2] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z. \hz. wtp_P) (\z. \hz. wtp_Q) (l_inr2 \x'. linP') linQ] = tpP in
+  let ([ ⊢ D] : [ ⊢ dual A A']) = [ ⊢ D] in
+  let [g, z:name, hz:hyp z A[] ⊢ wtp_inr x[..] hx (\x'. \hx'. wtp_P'[.., x', hx', z, hz])]
+    = [g, z:name, hz:hyp z A[] ⊢ wtp_P] in
+  let [g ⊢ hx'] = str_hyp [g, z:name, hz:hyp z A[] ⊢ hx] in
+   [g ⊢ wtp_inr x hx'
+    (\x'.\h'. wtp_pcomp D[] (\z.\hz. wtp_P') (\z.\hz. wtp_Q[.., z, hz]) linP'[..,x'] linQ[..])]
+| [g ⊢ κ&] ⇒
+  let [g ⊢ wtp_pcomp D[] (\z. \hz. wtp_P) (\z. \hz. wtp_Q) (l_choice2 (\x'.linP1) (\x'.linP2)) linQ] = tpP in
+  let [g, z:name, hz:hyp z _ ⊢ wtp_choice x[..] h (\x'.\h'.wtp_P1) (\x'.\h'.wtp_P2)] =
+  [g, z:name, hz:hyp z _ ⊢ wtp_P] in
+  let [g ⊢ h'] = str_hyp [g, z:name, hz:hyp z _ ⊢ h] in
+  [g ⊢ wtp_choice x h'
+    (\x'. \h'. wtp_pcomp D[] (\z.\hz. wtp_P1[..,z,hz,x',h']) (\z.\hz. wtp_Q[..,z,hz]) linP1[.., x'] linQ[..])
+    (\x'. \h'. wtp_pcomp D[] (\z.\hz. wtp_P2[..,z,hz,x',h']) (\z.\hz. wtp_Q[..,z,hz]) linP2[.., x'] linQ[..])]
+
+%  cut l/r
+| [g ⊢ β∥1 (\x. s_P)] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) linP linQ] = tpP in
+  let ([ ⊢ D] : [ ⊢ dual A A']) = [ ⊢ D] in
+  let [g, b:block x:name, h:hyp x A[] ⊢ wtp_P'] =
+    wtp_s [g, b:block x:name, h:hyp x A[] ⊢ wtp_P[..,b.1, b.2]]
+          [g, b:block x:name, h:hyp x A[] ⊢ s_P[..,b.1] ]
+    in
+  let [g ⊢ linP'] =
+    lin_s [g, x:name, h:hyp x A[] ⊢ wtp_P[..,x,h]]
+          [g, x:name ⊢ s_P[..,x]]
+          [g ⊢ linP]
+    in
+  [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P'[.., <x;h>]) (\x. \h. wtp_Q) linP' linQ]
+| [g ⊢ β∥2 (\x. s_Q)] ⇒
+  let [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q) linP linQ] = tpP in
+  let ([ ⊢ D] : [ ⊢ dual A A']) = [ ⊢ D] in
+  let [g, b:block x:name, h:hyp x A'[] ⊢ wtp_Q'] =
+    wtp_s [g, b:block x:name, h:hyp x A'[] ⊢ wtp_Q[..,b.1, b.2]]
+          [g, b:block x:name, h:hyp x A'[] ⊢ s_Q[..,b.1] ]
+    in
+  let [g ⊢ linQ'] =
+    lin_s [g, x:name, h:hyp x A'[] ⊢ wtp_Q[..,x,h]]
+          [g, x:name ⊢ s_Q[..,x]]
+          [g ⊢ linQ]
+    in
+  [g ⊢ wtp_pcomp D[] (\x. \h. wtp_P) (\x. \h. wtp_Q'[.., <x;h>]) linP linQ']
+| [g ⊢ β≡ ≡PQ ⇛QR ≡RS] ⇒
+  let [g ⊢ wtpQ] = wtp_s≡ tpP [g ⊢ ≡PQ] in
+  let [g ⊢ wtpR] = wtp_s [g ⊢ wtpQ] [g ⊢ ⇛QR] in
+  wtp_s≡ [g ⊢ wtpR] [g ⊢ ≡RS]
+;
+