X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week6.mdwn;h=f26285f3b9cb92768b509c3e93768166a3729a6a;hp=57158c6b92d1ac900cdb3a738a35a70c9eb29f64;hb=0bdafef1c31c5372b1b7d5a960e2a016754d5388;hpb=8e8edc03022be0da1621d6f1b418919c2637856e;ds=sidebyside

diff --git a/week6.mdwn b/week6.mdwn
index 57158c6b..f26285f3 100644
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -261,26 +261,26 @@ Axiom: -----------
 
 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>