diff --git a/Makefile b/Makefile
index 183facb..7b6132a 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,7 @@ SOURCES = log.ml version.ml config.dummy misc.ml heap.ml globals.ml error.ml \
 
 COQSRC = zenon.v zenon_coqbool.v zenon_equiv.v zenon_induct.v zenon_focal.v zenon_arith.v zenon_arith_reals.v
 
-DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk
+DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk zenon.dk
 
 DOCSRC =
 
diff --git a/dkprint.ml b/dkprint.ml
index 4a353b8..a182b6b 100644
--- a/dkprint.ml
+++ b/dkprint.ml
@@ -1,10 +1,56 @@
 open Printf
 open Dkterm
 
+(* taken on 19/07/24 from
+https://github.com/Deducteam/Dedukti/blob/master/parsing/lexer.mll *)
+let forbidden_idents = [
+  "(;"
+  ; ";)"
+  ; "."
+  ; ","
+  ; ":"
+  ; "=="
+  ; "["
+  ; "]"
+  ; "{"
+  ; "}"
+  ; "("
+  ; ")"
+  ; "-->"
+  ; "->"
+  ; "=>"
+  ; ":="
+  ; "Type"
+  ; "def"
+  ; "defac"
+  ; "defacu"
+  ; "injective"
+  ; "thm"
+  ; "private"
+  ; "require"
+  ; "assert"
+  ; "#NAME"
+  ; "#REQUIRE"
+  ; "#EVAL"
+  ; "#INFER"
+  ; "#CHECK"
+  ; "#CHECKNOT"
+  ; "#ASSERT"
+  ; "#ASSERTNOT"
+  ; "#PRINT"
+  ; "#GDT"
+  ]
+
+let escape_name s =
+  let id_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_]*$" in
+  if Str.string_match id_regex s 0
+    && List.for_all ((<>) s) forbidden_idents
+    then s else "{|" ^ s ^ "|}"
+
 let rec print_dk_type o t =
   match t with
-  | Dktypetype -> fprintf o "zen.type"
-  | Dktypeprop -> fprintf o "zen.prop"
+  | Dktypetype -> fprintf o "zenon.type"
+  | Dktypeprop -> fprintf o "zenon.prop"
   | Dkarrow (l, r) ->
      begin
        List.iter (fun x -> fprintf o "%a -> " print_dk_type x) l;
@@ -15,21 +61,28 @@ let rec print_dk_type o t =
 	     (get_var_newname var) print_dk_type t1 print_dk_type t2
   | Dkpi _ -> assert false
   | Dkproof (t) ->
-     fprintf o "zen.proof (%a)" print_dk_term t
-  | t -> fprintf o "zen.term (%a)" print_dk_zentype t
+     fprintf o "zenon.proof (%a)" print_dk_term t
+  | t -> fprintf o "zenon.term (%a)" print_dk_zentype t
 
 and print_dk_zentype o t =
   match t with
-  | Dktypeiota -> fprintf o "zen.iota"
+  | Dktypeiota -> fprintf o "zenon.iota"
   | t -> print_dk_term o t
 
 and print_dk_cst o t =
   match t with
   | "Is_true" -> fprintf o "dk_logic.ebP"
   | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite"
-  | s -> if !Globals.signature_name = "" then fprintf o "%s" s else
-    if Mltoll.is_meta s then fprintf o "zen.select (zen.iota)" else
-      fprintf o "%s.%s" !Globals.signature_name s
+  | s ->
+     if Mltoll.is_meta s then fprintf o "zenon.select (zenon.iota)"
+     else
+       begin
+         if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
+         else fprintf o "%s.%s" !Globals.signature_name (escape_name s);
+         if !Globals.conjecture <> ""
+            && not !Globals.check_axiom && Typetptp.is_axiom s then
+           fprintf o " __negated_conjecture_proof__"
+       end
 
 and print_dk_term o t =
   match t with
@@ -49,164 +102,164 @@ and print_dk_term o t =
        List.iter (fun x -> fprintf o " (%a)" print_dk_term x) l;
 (*       fprintf o "\n ";*)
      end
-  | Dkseq -> fprintf o "zen.seq"
+  | Dkseq -> fprintf o "zenon.seq"
   | Dknot (t) ->
-     fprintf o "zen.not\n (%a)" print_dk_term t
+     fprintf o "zenon.not\n (%a)" print_dk_term t
   | Dkand (t1, t2) ->
-     fprintf o "zen.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkor (t1, t2) ->
-     fprintf o "zen.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkimply (t1, t2) ->
-     fprintf o "zen.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkequiv (t1, t2) ->
-     fprintf o "zen.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkforall (t1, t2) ->
-     fprintf o "zen.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
+     fprintf o "zenon.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
   | Dkexists (t1, t2) ->
-     fprintf o "zen.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
+     fprintf o "zenon.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
   | Dkforalltype (t) ->
-     fprintf o "zen.foralltype\n (%a)" print_dk_term t
+     fprintf o "zenon.foralltype\n (%a)" print_dk_term t
   | Dkexiststype (t) ->
-     fprintf o "zen.existstype\n (%a)" print_dk_term t
-  | Dktrue -> fprintf o "zen.True"
-  | Dkfalse -> fprintf o "zen.False"
+     fprintf o "zenon.existstype\n (%a)" print_dk_term t
+  | Dktrue -> fprintf o "zenon.True"
+  | Dkfalse -> fprintf o "zenon.False"
   | Dkequal (t1, t2, t3) ->
-     fprintf o "zen.equal (%a)\n (%a)\n (%a)"
+     fprintf o "zenon.equal (%a)\n (%a)\n (%a)"
 	     print_dk_zentype t1
 	     print_dk_term t2
 	     print_dk_term t3
-  | DkRfalse (pr) -> fprintf o "zen.Rfalse\n (%a)" print_dk_term pr
-  | DkRnottrue (pr) -> fprintf o "zen.Rnottrue\n (%a)" print_dk_term pr
+  | DkRfalse (pr) -> fprintf o "zenon.Rfalse\n (%a)" print_dk_term pr
+  | DkRnottrue (pr) -> fprintf o "zenon.Rnottrue\n (%a)" print_dk_term pr
   | DkRaxiom (p, pr1, pr2) ->
-     fprintf o "zen.Raxiom\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Raxiom\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnoteq (a, t, pr) ->
-     fprintf o "zen.Rnoteq\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnoteq\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term t
 	     print_dk_term pr
   | DkReqsym (a, t, u, pr1, pr2) ->
-     fprintf o "zen.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term t
 	     print_dk_term u
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRcut (p, pr1, pr2) ->
-     fprintf o "zen.Rcut\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rcut\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotnot (p, pr1, pr2) ->
-     fprintf o "zen.Rnotnot\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotnot\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRand (p, q, pr1, pr2) ->
-     fprintf o "zen.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRor (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRimply (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRequiv (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRnotand (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRnotor (p, q, pr1, pr2) ->
-     fprintf o "zen.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotimply (p, q, pr1, pr2) ->
-     fprintf o "zen.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotequiv (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRex (a, p, pr1, pr2) ->
-     fprintf o "zen.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRall (a, p, t, pr1, pr2) ->
-     fprintf o "zen.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotex (a, p, t, pr1, pr2) ->
-     fprintf o "zen.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotall (a, p, pr1, pr2) ->
-     fprintf o "zen.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRextype (p, pr1, pr2) ->
-     fprintf o "zen.Rextype\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rextype\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRalltype (p, a, pr1, pr2) ->
-     fprintf o "zen.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_zentype a
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotextype (p, a, pr1, pr2) ->
-     fprintf o "zen.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_zentype a
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotalltype (p, pr1, pr2) ->
-     fprintf o "zen.Rnotalltype\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotalltype\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRsubst  (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
@@ -215,7 +268,7 @@ and print_dk_term o t =
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRconglr (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
@@ -224,7 +277,7 @@ and print_dk_term o t =
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRcongrl (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
diff --git a/globals.ml b/globals.ml
index 3ad0ad6..54e8a08 100644
--- a/globals.ml
+++ b/globals.ml
@@ -31,7 +31,7 @@ let debug_rwrt = ref false;;
 
 let output_sig = ref false;;
 let signature_name = ref "";;
-let neg_conj = ref "";;
+let conjecture = ref "";;
 let check_axiom = ref false;;
 
 let begin_comment() =
diff --git a/globals.mli b/globals.mli
index 6d918d4..f266da4 100644
--- a/globals.mli
+++ b/globals.mli
@@ -31,7 +31,7 @@ val debug_rwrt : bool ref;;
 
 val output_sig : bool ref;;
 val signature_name : string ref;;
-val neg_conj : string ref;;
+val conjecture : string ref;;
 val check_axiom : bool ref;;
 
 val begin_comment : unit -> string;;
diff --git a/lltodk.ml b/lltodk.ml
index d77097f..8aeaee5 100644
--- a/lltodk.ml
+++ b/lltodk.ml
@@ -1033,7 +1033,7 @@ let output oc phrases llp =
   let dkname = List.hd name in
   let prooftree = extract_prooftree llp in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-
+  fprintf oc "#REQUIRE zenon;\n\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dksigs;
   fprintf oc "\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dkctx;
@@ -1058,10 +1058,19 @@ let output_term oc phrases _ llp =
   in
   let dkgoal = translate_expr ngoal in
   let prooftree = extract_prooftree llp in
+  let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-  if !Globals.signature_name = "" then () else fprintf oc "def delta : zen.proof (%a) \n := \n " print_dk_term dkgoal;
-  fprintf oc "zen.nnpp (%a)\n\n(%a)"
-	  print_dk_term dkgoal
-	  print_dk_term dkproof;
-    if !Globals.signature_name = "" then () else fprintf oc ".";
+  fprintf oc "#REQUIRE zenon.\n";
+  if !Globals.signature_name <> "" then
+    begin
+      fprintf oc "#REQUIRE %s.\n" !Globals.signature_name;
+      fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name
+    end
+  else fprintf oc "\n[] %s --> " goal_name;
+  if !Globals.conjecture <> "" then
+    fprintf oc "__negated_conjecture_proof__ : \
+                zenon.proof (zenon.not Signature.conjecture) =>\n";
+  fprintf oc "zenon.nnpp (%a)\n(%a)"
+    print_dk_term dkgoal print_dk_term dkproof;
+  if !Globals.signature_name <> "" then fprintf oc ".";
   []
diff --git a/lltolp.ml b/lltolp.ml
index 83fab8c..ecedbdb 100644
--- a/lltolp.ml
+++ b/lltolp.ml
@@ -1064,15 +1064,15 @@ let output_term oc phrases _ llp =
   if !Globals.signature_name <> "" then
     fprintf oc "require %s as S;\n" !Globals.signature_name;
   fprintf oc "\nrule S.%s ↪ " goal_name;
-  let n = !Globals.neg_conj in
-  if n <> "" then fprintf oc "λ %s,\n" n;
+  if !Globals.conjecture <> "" then
+    fprintf oc "λ __negated_conjecture_proof__,";
   begin
     match dkgoal with
-    | Some g -> fprintf oc "\n  nnpp (%a)\n    (%a);\n"
-	          print_dk_term g
-	          print_dk_term dkproof
-    | None -> fprintf oc "\n %a;\n"
-	        print_dk_term dkproof
+    | Some g ->
+       fprintf oc "\n  nnpp (%a)\n    (%a);\n"
+         print_dk_term g print_dk_term dkproof
+    | None ->
+       fprintf oc "\n %a;\n" print_dk_term dkproof
   end;
   []
 
diff --git a/lpprint.ml b/lpprint.ml
index 1142c48..9c4b968 100644
--- a/lpprint.ml
+++ b/lpprint.ml
@@ -79,7 +79,6 @@ let escape_name s =
     && List.for_all ((<>) s) forbidden_idents
     then s else "{|" ^ s ^ "|}"
 
-
 let rec print_dk_type_aux o (t, var_context) =
   match t with
   | Dktypetype -> fprintf o "Set"
@@ -108,13 +107,14 @@ and print_dk_cst o t =
   | "Is_true" -> fprintf o "dk_logic.ebP"
   | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite"
   | s ->
-     if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
-     else if Mltoll.is_meta s then fprintf o "select ι"
+     if Mltoll.is_meta s then fprintf o "select ι"
      else
        begin
-         fprintf o "S.%s" (escape_name s);
-         if !Globals.neg_conj <> "" && not !Globals.check_axiom
-            && Typetptp.is_axiom s then fprintf o "%s" !Globals.neg_conj
+         if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
+         else fprintf o "S.%s" (escape_name s);
+         if !Globals.conjecture <> ""
+            && not !Globals.check_axiom && Typetptp.is_axiom s then
+           fprintf o " __negated_conjecture_proof__"
        end
 
 and print_dk_term_aux o (t, var_context) =
diff --git a/main.ml b/main.ml
index b624342..4576e2a 100644
--- a/main.ml
+++ b/main.ml
@@ -182,9 +182,7 @@ let argspec = [
 				  opt_level := 0;
 				  Globals.output_lp := true),
             "           print the proof in lambdapi term format";
-  "-conj", Arg.Unit (fun () -> Globals.neg_conj :=
-                                 (* keep space at the beginning *)
-                                 " __negated_conjecture__"),
+  "-conj", Arg.Unit (fun () -> Globals.conjecture := "conjecture"),
       "              indicate whether there is an explicit conjecture";
   "-check-axiom", Arg.Unit (fun () -> Globals.check_axiom := true),
       "       indicate whether this is a GDV leaf problem";
diff --git a/zenon.dk b/zenon.dk
new file mode 100644
index 0000000..d317209
--- /dev/null
+++ b/zenon.dk
@@ -0,0 +1,169 @@
+(; propositions ;)
+prop : Type.
+True : prop.
+False : prop.
+imp : prop -> prop -> prop.
+def not : prop -> prop := p : prop => imp p False.
+and : prop -> prop -> prop.
+or : prop -> prop -> prop.
+def eqv : prop -> prop -> prop := p : prop => q : prop => and (imp p q) (imp q p).
+
+(; sorts ;)
+type : Type.
+def iota : type.
+
+(; interpretation of sorts as types ;)
+injective term : type -> Type.
+
+(; axiom saying that every sort is inhabited ;)
+def select : a : type -> term a.
+
+(; sorted equality and quantifiers ;)
+equal : a : type -> term a -> term a -> prop.
+forall : a : type -> (term a -> prop) -> prop.
+exists : a : type -> (term a -> prop) -> prop.
+
+(; interpretation of propositions as types ;)
+injective proof : prop -> Type.
+[p, q] proof (imp p q) --> proof p -> proof q.
+[a, p] proof (forall a p) --> x : term a -> proof (p x).
+
+(; axiom equivalent to the excluded middle ;)
+def nnpp : p : prop -> proof (not (not p)) -> proof p.
+
+(; epsilon ;)
+def epsilon : a : type -> p : (term a -> prop) -> term a.
+def epsilon_intro : a : type -> p : (term a -> prop) -> proof (exists a p) -> proof (p (epsilon a p)).
+
+(; Zenon rules ;)
+
+def Rfalse : proof False -> proof False.
+
+def Rnottrue : proof (not True) -> proof False.
+
+def Raxiom : p : prop -> proof p -> proof (not p) -> proof False.
+
+def Rnoteq : a : type -> t : term a -> proof (not (equal a t t)) -> proof False.
+
+def Reqsym : a : type ->
+             t : term a ->
+             u : term a ->
+             proof (equal a t u) ->
+             proof (not (equal a u t)) ->
+             proof False.
+
+def Rcut : p : prop ->
+           (proof p -> proof False) ->
+           (proof (not p) -> proof False) ->
+           proof False.
+
+def Rnotnot : p : prop ->
+              (proof p -> proof False) ->
+              proof (not (not p)) ->
+              proof False.
+
+def Rand : p : prop ->
+           q : prop ->
+           (proof p -> proof q -> proof False) ->
+           proof (and p q) ->
+           proof False.
+
+def Ror : p : prop ->
+          q : prop ->
+          (proof p -> proof False) ->
+          (proof q -> proof False) ->
+          proof (or p q) ->
+          proof False.
+
+def Rimply : p : prop ->
+             q : prop ->
+             (proof (not p) -> proof False) ->
+             (proof q -> proof False) ->
+             proof (imp p q) ->
+             proof False.
+
+def Requiv : p : prop ->
+             q : prop ->
+             (proof (not p) -> proof (not q) -> proof False) ->
+             (proof p -> proof q -> proof False) ->
+             proof (eqv p q) ->
+             proof False.
+
+def Rnotand : p : prop ->
+              q : prop ->
+              (proof (not p) -> proof False) ->
+              (proof (not q) -> proof False) ->
+              proof (not (and p q)) ->
+              proof False.
+
+def Rnotor : p : prop ->
+             q : prop ->
+             (proof (not p) -> proof (not q) -> proof False) ->
+             proof (not (or p q)) ->
+             proof False.
+
+def Rnotimply : p : prop ->
+                q : prop ->
+                (proof p -> proof (not q) -> proof False) ->
+                proof (not (imp p q)) ->
+                proof False.
+
+def Rnotequiv : p : prop ->
+                q : prop ->
+                (proof (not p) -> proof q -> proof False) ->
+                (proof p -> proof (not q) -> proof False) ->
+                proof (not (eqv p q)) ->
+                proof False.
+
+def Rex : a : type ->
+          p : (term a -> prop) ->
+          (t : term a -> proof (p t) -> proof False) ->
+          proof (exists a p) ->
+          proof False.
+
+def Rall : a : type ->
+           p : (term a -> prop) ->
+           t : term a ->
+           (proof (p t) -> proof False) ->
+           proof (forall a p) ->
+           proof False.
+
+def Rnotex : a : type ->
+             p : (term a -> prop) ->
+             t : term a ->
+             (proof (not (p t)) -> proof False) ->
+             proof (not (exists a p)) ->
+             proof False.
+
+def Rnotall : a : type ->
+              p : (term a -> prop) ->
+              (t : term a -> proof (not (p t)) -> proof False) ->
+              proof (not (forall a p)) ->
+              proof False.
+
+def Rsubst : a : type ->
+             p : (term a -> prop) ->
+             t1 : term a ->
+             t2 : term a ->
+             (proof (not (equal a t1 t2)) -> proof False) ->
+             (proof (p t2) -> proof False) ->
+             proof (p t1) ->
+             proof False.
+
+def Rconglr : a : type ->
+              p : (term a -> prop) ->
+              t1 : term a ->
+              t2 : term a ->
+              (proof (p t2) -> proof False) ->
+              proof (p t1) ->
+              proof (equal a t1 t2) ->
+              proof False.
+
+def Rcongrl : a : type ->
+              p : (term a -> prop) ->
+              t1 : term a ->
+              t2 : term a ->
+              (proof (p t2) -> proof False) ->
+              proof (p t1) ->
+              proof (equal a t2 t1) ->
+              proof False.