Update to Dedukti version 2.2.1 new syntax

cc.dk

-#NAME cc
+#NAME cc.
 (; Calculus of Construction embedded into Lambda-Pi Modulo ;)
 
 uT : Type.

dk_binary_nat.dk

-#NAME dk_binary_nat
+#NAME dk_binary_nat.
 
 UNat : Type := dk_nat.Nat.
 Bool : Type := dk_bool.Bool.

dk_bool.dk

-#NAME dk_bool
+#NAME dk_bool.
 
 (; Bool ;)
 (; Declaration ;)
@@ -6,8 +6,8 @@ bool : cc.uT.
 Bool : Type := cc.eT bool.
 
 (; Constructors ;)
-true : Bool.
-false : Bool.
+{true} : Bool.
+{false} : Bool.
 
 (; Pattern-matching ;)
 match :

dk_builtins.dk

-#NAME dk_builtins
+#NAME dk_builtins.
 (; This file defines basic types for the translation of FoCaLize
 standard library into Dedukti ;) 
 

dk_char.dk

-#NAME dk_char
+#NAME dk_char.
 (; 7bits (ascii) characters ;)
 
 char : cc.uT := dk_machine_int.Mint dk_nat.7.

dk_fail.dk

-#NAME dk_fail
+#NAME dk_fail.
 
 fail : A : cc.uT -> cc.eT A.

dk_int.dk

-#NAME dk_int
+#NAME dk_int.
 Nat : Type := dk_nat.Nat.
 O : Nat := dk_nat.O.
 S : Nat -> Nat := dk_nat.S.

dk_list.dk

-#NAME dk_list
+#NAME dk_list.
 
 (; Polymorphic lists ;)
-list : cc.uT -> cc.uT.
+{list} : cc.uT -> cc.uT.
 List := A : cc.uT => cc.eT (list A).
 
 (; Constructors ;)
-nil : A : cc.uT -> List A.
-cons : A : cc.uT -> cc.eT A -> List A -> List A.
+{nil} : A : cc.uT -> List A.
+{cons} : A : cc.uT -> cc.eT A -> List A -> List A.
 
 (; Case distinction ;)
 match : A : cc.uT ->
@@ -20,7 +20,7 @@ match : A : cc.uT ->
  P : List A -> cc.uT,
  Hnil : cc.eT (P (nil A)),
  Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))]
-    match _ P Hnil Hcons (nil A) --> Hnil
+    match A P Hnil Hcons (nil A) --> Hnil
 
 [A : cc.uT,
  P : List A -> cc.uT,
@@ -28,7 +28,7 @@ match : A : cc.uT ->
  Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l)),
  a : cc.eT A,
  l : List A]
-    match _ P Hnil Hcons (cons A a l) --> Hcons a l.
+    match A P Hnil Hcons (cons A a l) --> Hcons a l.
 
 (; Non dependant case distinction ;)
 simple_match : A : cc.uT ->
@@ -45,11 +45,11 @@ simple_match : A : cc.uT ->
 (; Append ;)
 append : A : cc.uT -> List A -> List A -> List A.
 [ A : cc.uT, l2 : List A ]
-    append A (nil _) l2 --> l2
+    append A (nil A) l2 --> l2
 [ A : cc.uT, a1 : cc.eT A, l1 : List A, l2 : List A ]
-    append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2)
+    append A (cons A a1 l1) l2 --> cons A a1 (append A l1 l2)
 [ A : cc.uT, l1 : List A, l2 : List A, l3 : List A]
-    append A l1 (append _ l2 l3) --> append A (append A l1 l2) l3.
+    append A l1 (append A l2 l3) --> append A (append A l1 l2) l3.
 
 (; Map ;)
 map : A : cc.uT ->
@@ -57,18 +57,18 @@ map : A : cc.uT ->
       (cc.eT A -> cc.eT B) -> List A -> List B.
 [A : cc.uT,
  B : cc.uT,
- f : cc.eT A -> cc.eT B] map A B f (nil _) --> nil B
+ f : cc.eT A -> cc.eT B] map A B f (nil A) --> nil B
 [A : cc.uT,
  B : cc.uT,
  f : cc.eT A -> cc.eT B,
  a : cc.eT A,
- l : cc.eT (list A)] map A B f (cons _ a l) --> cons B (f a) (map A B f l)
+ l : cc.eT (list A)] map A B f (cons A a l) --> cons B (f a) (map A B f l)
 [A : cc.uT,
  B : cc.uT,
  C : cc.uT,
  f : cc.eT A -> cc.eT B,
  g : cc.eT B -> cc.eT C,
- l : cc.eT (list A)] map _ C g (map A B f l) --> map A C (x : cc.eT A => g (f x)) l.
+ l : cc.eT (list A)] map B C g (map A B f l) --> map A C (x : cc.eT A => g (f x)) l.
 
 mem : A : cc.uT ->
       (cc.eT A -> cc.eT A -> cc.eT dk_bool.bool) ->
@@ -76,9 +76,9 @@ mem : A : cc.uT ->
       List A ->
       cc.eT dk_bool.bool.
 [ A : cc.uT, eq : cc.eT A -> cc.eT A -> cc.eT dk_bool.bool, a : cc.eT A ]
-    mem A eq a (nil _) --> dk_bool.false
+    mem A eq a (nil A) --> dk_bool.false
 [ A : cc.uT, eq : cc.eT A -> cc.eT A -> cc.eT dk_bool.bool, a1 : cc.eT A, a2 : cc.eT A, l : cc.eT (list A) ]
-    mem A eq a1 (cons _ a2 l) --> dk_bool.or (eq a1 a2) (mem A eq a1 l).
+    mem A eq a1 (cons A a2 l) --> dk_bool.or (eq a1 a2) (mem A eq a1 l).
 
 
 
@@ -87,11 +87,19 @@ map_id :
   l : cc.eT (list B) ->
   dk_logic.eP (dk_logic.equal (list B) (map B B (x : cc.eT B => x) l) l).
 [B : cc.uT]
-    map_id _ (nil B) --> dk_logic.refl (list B) (nil B)
+    map_id B (nil B) --> dk_logic.refl (list B) (nil B)
 [A : cc.uT,
  a : cc.eT A,
  l : cc.eT (list A)]
-    map_id _ (cons A a l) --> dk_logic.equal_congr (list A) (list A) (cons A a) (map A A (x : cc.eT A => x) l) l (map_id A l).
+    map_id A (cons A a l)
+      -->
+    dk_logic.equal_congr
+      (list A)
+      (list A)
+      (cons A a)
+      (map A A (x : cc.eT A => x) l)
+      l
+        (map_id A l).
 
 
 dlist : A : cc.uT -> cc.eT A -> cc.uT.

dk_logic.dk

-#NAME dk_logic
+#NAME dk_logic.
 
 (; Impredicative prop ;)
 
@@ -74,17 +74,17 @@ or_elim : f1 : Prop ->
 (; cut elimination ;)
 [f1 : Prop, f2 : Prop,
  H1 : eP f1, H2 : eP f2]
-    and_elim1 _ _ (and_intro f1 f2 H1 H2) --> H1.
+    and_elim1 f1 f2 (and_intro f1 f2 H1 H2) --> H1.
 [f1 : Prop, f2 : Prop,
  H1 : eP f1, H2 : eP f2]
-    and_elim2 _ _ (and_intro f1 f2 H1 H2) --> H2.
+    and_elim2 f1 f2 (and_intro f1 f2 H1 H2) --> H2.
 
 [ f1 : Prop, f2 : Prop, f3 : Prop,
   H1 : eP f1, H13 : eP (imp f1 f3) ]
-    or_elim _ _ f3 (or_intro1 f1 f2 H1) H13 _ --> H13 H1
+    or_elim f1 f2 f3 (or_intro1 f1 f2 H1) H13 _ --> H13 H1
 [ f1 : Prop, f2 : Prop, f3 : Prop,
   H2 : eP f2, H23 : eP (imp f2 f3) ]
-    or_elim _ _ f3 (or_intro2 f1 f2 H2) _ H23 --> H23 H2.
+    or_elim f1 f2 f3 (or_intro2 f1 f2 H2) _ H23 --> H23 H2.
 
 eqv_intro := f1 : Prop =>
              f2 : Prop =>
@@ -391,9 +391,10 @@ bool_ifnot_intro : b : cc.eT dk_bool.bool ->
                    cc.eT (P (dk_bool.ite A b a1 a2)).
 [ A : cc.uT,
   a1 : cc.eT A,
+  a2 : cc.eT A,
   P : cc.eT A -> cc.uT,
-  H : cc.eT (P a1) ]
-    bool_ifnot_intro dk_bool.false _ A a1 _ P H --> H
+  H : cc.eT (P a2) ]
+    bool_ifnot_intro dk_bool.false _ A a1 a2 P H --> H
 [ H : FalseT,
   A : cc.uT,
   a1 : cc.eT A,
@@ -411,9 +412,10 @@ bool_ifnot_elim : b : cc.eT dk_bool.bool ->
                   cc.eT (P a2).
 [ A : cc.uT,
   a1 : cc.eT A,
+  a2 : cc.eT A,
   P : cc.eT A -> cc.uT,
-  H : cc.eT (P a1) ]
-    bool_ifnot_elim dk_bool.false _ A a1 _ P H --> H
+  H : cc.eT (P a2) ]
+    bool_ifnot_elim dk_bool.false _ A a1 a2 P H --> H
 [ H : FalseT,
   A : cc.uT,
   a1 : cc.eT A,

dk_machine_int.dk

-#NAME dk_machine_int
+#NAME dk_machine_int.
 Bool : Type := dk_bool.Bool.
 
 UNat : Type := dk_nat.Nat.
@@ -23,40 +23,40 @@ bound : N : UNat -> MInt N.
 
 (; cast ;)
 downcast : N : UNat -> MInt (US N) -> MInt N.
-[n : MInt (US UO)] downcast _ n --> O
+[n : MInt (US UO)] downcast dk_nat.O n --> O
 [N : UNat, n : MInt (US N)]
-    downcast _ (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
+    downcast (dk_nat.S N) (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
 [N : UNat, n : MInt (US N)]
-    downcast _ (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
+    downcast (dk_nat.S N) (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
 
 double : N : UNat ->     MInt N -> MInt N
        := N : UNat => n : MInt N => downcast N (S0 N n).
 
 succ : N : UNat -> MInt N -> MInt N.
-[] succ _ O --> O
-[ N : UNat, n : MInt N ] succ _ (S0 N n) --> S1 N n
-[ N : UNat, n : MInt N ] succ _ (S1 N n) --> S0 N (succ N n).
+[] succ dk_nat.O O --> O
+[ N : UNat, n : MInt N ] succ (dk_nat.S N) (S0 N n) --> S1 N n
+[ N : UNat, n : MInt N ] succ (dk_nat.S N) (S1 N n) --> S0 N (succ N n).
 
 pred : N : UNat -> MInt N -> MInt N.
-[] pred _ O --> O
-[ N : UNat, n : MInt N ] pred _ (S1 N n) --> S0 N n
-[ N : UNat, n : MInt N ] pred _ (S0 N n) --> S1 N (pred N n).
+[] pred dk_nat.O O --> O
+[ N : UNat, n : MInt N ] pred (dk_nat.S N) (S1 N n) --> S0 N n
+[ N : UNat, n : MInt N ] pred (dk_nat.S N) (S0 N n) --> S1 N (pred N n).
 
 plus : N : UNat -> MInt N -> MInt N -> MInt N.
-[ ] plus _ O O --> O
+[ ] plus dk_nat.O O O --> O
 [ N : UNat, n : MInt N, m : MInt N ]
-    plus _ (S0 _ n) (S0 N m) --> S0 N (plus N n m)
+    plus (dk_nat.S N) (S0 N n) (S0 N m) --> S0 N (plus N n m)
 [ N : UNat, n : MInt N, m : MInt N ]
-    plus _ (S0 _ n) (S1 N m) --> S1 N (plus N n m)
+    plus (dk_nat.S N) (S0 N n) (S1 N m) --> S1 N (plus N n m)
 [ N : UNat, n : MInt N, m : MInt N ]
-    plus _ (S1 _ n) (S0 N m) --> S1 N (plus N n m)
+    plus (dk_nat.S N) (S1 N n) (S0 N m) --> S1 N (plus N n m)
 [ N : UNat, n : MInt N, m : MInt N ]
-    plus _ (S1 _ n) (S1 N m) --> S0 N (succ N (plus N n m)).
+    plus (dk_nat.S N) (S1 N n) (S1 N m) --> S0 N (succ N (plus N n m)).
 
 complement : N : UNat -> MInt N -> MInt N.
-[] complement _ O --> O
-[ N : UNat, n : MInt N ] complement _ (S0 N n) --> S1 N (complement N n)
-[ N : UNat, n : MInt N ] complement _ (S1 N n) --> S0 N (complement N n).
+[] complement dk_nat.O O --> O
+[ N : UNat, n : MInt N ] complement (dk_nat.S N) (S0 N n) --> S1 N (complement N n)
+[ N : UNat, n : MInt N ] complement (dk_nat.S N) (S1 N n) --> S0 N (complement N n).
 
 opp : N : UNat -> MInt N -> MInt N.
 [ N : UNat, n : MInt N ] opp N n --> succ N (complement N n).
@@ -66,21 +66,21 @@ sub : N : UNat -> MInt N -> MInt N -> MInt N.
 
 (; Product ;)
 mult : N : UNat -> MInt N -> MInt N -> MInt N.
-[ ] mult _ O O --> O
+[ ] mult dk_nat.O O O --> O
 [ N : UNat, n : MInt N, m : MInt N ]
-    mult _ (S0 _ n) (S0 N m)
+    mult (dk_nat.S N) (S0 N n) (S0 N m)
       -->
     double (US N) (S0 N (mult N n m))
 [ N : UNat, n : MInt N, m : MInt N ]
-    mult _ (S0 _ n) (S1 N m)
+    mult (dk_nat.S N) (S0 N n) (S1 N m)
       -->
     S0 N (plus N m (double N (mult N n m)))
 [ N : UNat, n : MInt N, m : MInt N ]
-    mult _ (S1 _ n) (S0 N m)
+    mult (dk_nat.S N) (S1 N n) (S0 N m)
       -->
     S0 N (plus N n (double N (mult N n m)))
 [ N : UNat, n : MInt N, m : MInt N ]
-    mult _ (S1 _ n) (S1 N m)
+    mult (dk_nat.S N) (S1 N n) (S1 N m)
       -->
     S1 N (plus N (double N (mult N m n)) (plus N n m)).
 
@@ -88,51 +88,51 @@ mult : N : UNat -> MInt N -> MInt N -> MInt N.
 equal : N : UNat -> MInt N -> MInt N -> Bool.
 [ N : UNat, n : MInt N ] equal N n n --> dk_bool.true
 [ N : UNat, n : MInt N, m : MInt N ]
-    equal _ (S0 _ n) (S0 N m) --> equal N n m
+    equal (dk_nat.S N) (S0 N n) (S0 N m) --> equal N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    equal _ (S1 _ n) (S1 N m) --> equal N n m
+    equal (dk_nat.S N) (S1 N n) (S1 N m) --> equal N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    equal _ (S0 _ n) (S1 N m) --> dk_bool.false
+    equal (dk_nat.S N) (S0 N n) (S1 N m) --> dk_bool.false
 [ N : UNat, n : MInt N, m : MInt N ]
-    equal _ (S1 _ n) (S0 N m) --> dk_bool.false.
+    equal (dk_nat.S N) (S1 N n) (S0 N m) --> dk_bool.false.
 
 (; unsigned comparison ;)
 unsigned_lt : N : UNat -> MInt N -> MInt N -> Bool.
 unsigned_leq : N : UNat -> MInt N -> MInt N -> Bool.
 
-[] unsigned_lt _ O O --> dk_bool.false
+[] unsigned_lt dk_nat.O O O --> dk_bool.false
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_lt _ (S0 _ n) (S0 N m)
+    unsigned_lt (dk_nat.S N) (S0 N n) (S0 N m)
       -->
     unsigned_lt N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_lt _ (S1 _ n) (S1 N m)
+    unsigned_lt (dk_nat.S N) (S1 N n) (S1 N m)
       -->
     unsigned_lt N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_lt _ (S0 _ n) (S1 N m)
+    unsigned_lt (dk_nat.S N) (S0 N n) (S1 N m)
       -->
     unsigned_leq N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_lt _ (S1 _ n) (S0 N m)
+    unsigned_lt (dk_nat.S N) (S1 N n) (S0 N m)
       -->
     unsigned_lt N n m.
 
-[] unsigned_leq _ O O --> dk_bool.true
+[] unsigned_leq dk_nat.O O O --> dk_bool.true
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_leq _ (S0 _ n) (S0 N m)
+    unsigned_leq (dk_nat.S N) (S0 N n) (S0 N m)
       -->
     unsigned_leq N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_leq _ (S1 _ n) (S1 N m)
+    unsigned_leq (dk_nat.S N) (S1 N n) (S1 N m)
       -->
     unsigned_leq N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_leq _ (S0 _ n) (S1 N m)
+    unsigned_leq (dk_nat.S N) (S0 N n) (S1 N m)
       -->
     unsigned_leq N n m
 [ N : UNat, n : MInt N, m : MInt N ]
-    unsigned_leq _ (S1 _ n) (S0 N m)
+    unsigned_leq (dk_nat.S N) (S1 N n) (S0 N m)
       -->
     unsigned_lt N n m.
 
@@ -144,11 +144,11 @@ unsigned_geq : N : UNat -> MInt N -> MInt N -> Bool
 
 (; signed comparison ;)
 positive : N : UNat -> MInt N -> Bool.
-[] positive _ O --> dk_bool.true
-[] positive _ (S0 _ O) --> dk_bool.true
-[] positive _ (S1 _ O) --> dk_bool.false
-[ N : UNat, n : MInt N ] positive _ (S0 N n) --> positive N n
-[ N : UNat, n : MInt N ] positive _ (S1 N n) --> positive N n.
+[] positive dk_nat.O O --> dk_bool.true
+[] positive (dk_nat.S dk_nat.O) (S0 dk_nat.O O) --> dk_bool.true
+[] positive (dk_nat.S dk_nat.O) (S1 dk_nat.O O) --> dk_bool.false
+[ N : UNat, n : MInt N ] positive (dk_nat.S N) (S0 N n) --> positive N n
+[ N : UNat, n : MInt N ] positive (dk_nat.S N) (S1 N n) --> positive N n.
 
 signed_leq : N : UNat ->
              n : MInt N ->

dk_monads.dk

-#NAME dk_monads
+#NAME dk_monads.
 
 (; Monadic operators ;)
 return :
@@ -53,12 +53,12 @@ comp :
   B : cc.uT ,
   a : cc.eT A ,
   f : (cc.eT A -> cc.eT (M B)) ]
-    bind M A B (return _ _ a) f --> f a.
+    bind M A B (return M A a) f --> f a.
 
 [ M : (cc.uT -> cc.uT),
   A : cc.uT,
   m : cc.eT (M A) ]
-    bind M _ _ m (return M A) --> m.
+    bind M A A m (return M A) --> m.
 
 [ M : (cc.uT -> cc.uT),
   A : cc.uT,
@@ -67,7 +67,7 @@ comp :
   f : (cc.eT A -> cc.eT (M B)),
   g : (cc.eT B -> cc.eT (M C)),
   m : cc.eT (M A) ]
-    bind M B C (bind _ A _ m f) g
+    bind M B C (bind M A B m f) g
       -->
     bind M A C m (comp M A B C f g).
 
@@ -83,10 +83,10 @@ Some : A : cc.uT -> cc.eT A -> cc.eT (option A).
 
 [A : cc.uT,
  B : cc.uT, f : cc.eT A -> cc.eT (option B)]
-    bind option A B (None _) f --> None B
+    bind option A B (None A) f --> None B
 [A : cc.uT, a : cc.eT A,
  B : cc.uT, f : cc.eT A -> cc.eT (option B)]
-    bind option A B (Some _ a) f --> f a.
+    bind option A B (Some A a) f --> f a.
 
 (; list type ;)
 
@@ -96,12 +96,12 @@ Cons : A : cc.uT -> cc.eT A -> cc.eT (list A) -> cc.eT (list A).
 
 append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
 [A : cc.uT, l2 : cc.eT (list A)]
-    append A (Nil _) l2 --> l2
+    append A (Nil A) l2 --> l2
 [A : cc.uT, a : cc.eT A, l1 : cc.eT (list A), l2 : cc.eT (list A)]
-    append A (Cons _ a l1) l2 --> Cons A a (append A l1 l2)
+    append A (Cons A a l1) l2 --> Cons A a (append A l1 l2)
 (; Let's add a third rule to get append l Nil = l ;)
 [A : cc.uT, l1 : cc.eT (list A)]
-    append A l1 (Nil _) --> l1.
+    append A l1 (Nil A) --> l1.
 
 (; the list monad ;)
 
@@ -109,7 +109,7 @@ append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
 
 [A : cc.uT,
  B : cc.uT, f : cc.eT A -> cc.eT (list B)]
-    bind list A B (Nil _) f --> Nil B
+    bind list A B (Nil A) f --> Nil B
 [A : cc.uT, a : cc.eT A, l : cc.eT (list A),
  B : cc.uT, f : cc.eT A -> cc.eT (list B)]
-    bind list A B (Cons _ a l) f --> append B (f a) (bind list A B l f).
+    bind list A B (Cons A a l) f --> append B (f a) (bind list A B l f).

dk_nat.dk

-#NAME dk_nat
+#NAME dk_nat.
 Bool : Type := dk_bool.Bool.
 
 nat : cc.uT.
 Nat : Type := cc.eT nat.
 
-O : Nat.
-S : Nat -> Nat.
+{O} : Nat.
+{S} : Nat -> Nat.
 
 (; Order ;)
 lt : Nat -> Nat -> Bool.

dk_opt.dk

-#NAME dk_opt
+#NAME dk_opt.
 
 (; options ;)
 option : cc.uT -> cc.uT.
@@ -18,13 +18,13 @@ match_option : A : cc.uT ->
  P : Option A -> cc.uT,
  Hnone : cc.eT (P (None A)),
  Hsome : a : cc.eT A -> cc.eT (P (Some A a))]
-    match_option A P Hnone Hsome (None _) --> Hnone
+    match_option A P Hnone Hsome (None A) --> Hnone
 [A : cc.uT,
  P : Option A -> cc.uT,
  Hnone : cc.eT (P (None A)),
  Hsome : a : cc.eT A -> cc.eT (P (Some A a)),
  a : cc.eT A]
-    match_option A P Hnone Hsome (Some _ a) --> Hsome a.
+    match_option A P Hnone Hsome (Some A a) --> Hsome a.
 
 simple_match_option : A : cc.uT ->
                       return : cc.uT ->

dk_string.dk

-#NAME dk_string
+#NAME dk_string.
 (; lists of ascii characters ;)
 
-string := dk_list.list dk_char.char.
+(; (dk_machine_int.Mint (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))))) ;)
+
+string : cc.uT.
 String := cc.eT string.
+nil : String.
+cons : dk_char.Char -> String -> String.
+
+
 equal : String -> String -> dk_bool.Bool.
+
 [ s : String ] equal s s --> dk_bool.true
-[ ] equal (dk_list.nil _) (dk_list.cons _ _ _) --> dk_bool.false
-[ ] equal (dk_list.cons _ _ _) (dk_list.nil _) --> dk_bool.false
+[ ] equal nil (cons _ _)
+      --> dk_bool.false
+[ ] equal (cons _ _) nil
+      --> dk_bool.false
 [ c1 : dk_char.Char, s1 : String,
   c2 : dk_char.Char, s2 : String ]
-    equal (dk_list.cons _ c1 s1) (dk_list.cons _ c2 s2)
+    equal (cons c1 s1)
+          (cons c2 s2)
       -->
     dk_bool.and (dk_char.equal c1 c2) (equal s1 s2).
-
-nil := dk_list.nil dk_char.char.
-cons := dk_list.cons dk_char.char.

dk_tuple.dk

-#NAME dk_tuple
+#NAME dk_tuple.
 
 tuple : cc.uT -> cc.uT -> cc.uT.
 Tuple : cc.uT -> cc.uT -> Type.
@@ -14,9 +14,9 @@ fst : A : cc.uT -> B : cc.uT -> Tuple A B -> cc.eT A.
 snd : A : cc.uT -> B : cc.uT -> Tuple A B -> cc.eT B.
 
 [A : cc.uT, B : cc.uT, a : cc.eT A, b : cc.eT B]
-    fst _ _ (cpl A B a b) --> a.
+    fst A B (cpl A B a b) --> a.
 [A : cc.uT, B : cc.uT, a : cc.eT A, b : cc.eT B]
-    snd _ _ (cpl A B a b) --> b.
+    snd A B (cpl A B a b) --> b.
 
 dTuple : A : cc.uT -> (cc.eT A -> cc.uT) -> cc.uT.
 DTuple : A : cc.uT -> (cc.eT A -> cc.uT) -> Type.
@@ -38,6 +38,6 @@ dsnd : A : cc.uT ->
        cc.eT (B (dfst A B t)).
 
 [A : cc.uT, B : (cc.eT A -> cc.uT), a : cc.eT A, b : cc.eT (B a)]
-    dfst _ _ (dcpl A B a b) --> a.
+    dfst A B (dcpl A B a b) --> a.
 [A : cc.uT, B : (cc.eT A -> cc.uT), a : cc.eT A, b : cc.eT (B a)]
-    dsnd _ _ (dcpl A B a b) --> b.
+    dsnd A B (dcpl A B a b) --> b.