Rename the term constructors

syntax.sig

@@ -1,4 +1,5 @@
 nat  : Type
+PTm(VarPTm) : Type
 Tm(VarTm) : Type
 PTag : Type
 TTag : Type
@@ -8,14 +9,21 @@ PL : PTag
 PR : PTag
 TPi : TTag
 TSig : TTag
+
+PAbs : (bind PTm in PTm) -> PTm
+PApp : PTm -> PTm -> PTm
+PPair : PTm -> PTm -> PTm
+PProj : PTag -> PTm -> PTm
+PConst : TTag -> PTm
+PUniv : nat -> PTm
+PBot : PTm
+
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
-Const : TTag -> Tm
 Univ : nat -> Tm
-Bot : Tm
 BVal : bool -> Tm
 Bool : Tm
 If : Tm -> Tm -> Tm -> Tm

theories/diagram.txt

@@ -18,3 +18,25 @@ a0 >> a1
 |     |
 v     v
 b0 >> b1
+
+
+prov x (x, x)
+
+prov x b
+
+
+a => b
+
+prov x a
+
+prov y b
+
+prov x c
+prov y c
+
+extract c = x
+extract c = y
+
+prov x b
+
+pr