Structural Rules:
-Exchange: Γ, x:A, y:B, Δ |- R:C
- -------------------------------
+ Γ, x:A, y:B, Δ |- R:C
+Exchange: -------------------------------
Γ, y:B, x:A, Δ |- R:C
-Contraction: Γ, x:A, x:A |- R:B
- --------------------------
+ Γ, x:A, x:A |- R:B
+Contraction: --------------------------
Γ, x:A |- R:B
-Weakening: Γ |- R:B
- ---------------------
+ Γ |- R:B
+Weakening: ---------------------
Γ, x:A |- R:B [x chosen fresh]
Logical Rules:
---> I: Γ, x:A |- R:B
- -------------------------
+ Γ, x:A |- R:B
+--> I: -------------------------
Γ |- \xM:A --> B
---> E: Γ |- f:(A --> B) Γ |- x:A
- -------------------------------------
+ Γ |- f:(A --> B) Γ |- x:A
+--> E: -------------------------------------
Γ |- (fx):B
</pre>