diff --git a/dune-workspace b/dune-workspace
new file mode 100644
index 000000000..e69de29bb
diff --git a/lambdap.elpi b/lambdap.elpi
new file mode 100644
index 000000000..b4e68e9fb
--- /dev/null
+++ b/lambdap.elpi
@@ -0,0 +1,1307 @@
+% automatically generated
+
+% ---- Lambdapi datatypes ----
+
+% A symbol
+typeabbrev symbol (ctype "symbol").
+
+
+
+kind term type.
+type typ term.
+type kin term.
+type symb symbol -> term.
+type appl term -> term -> term.
+type abst term -> (term -> term) -> term.
+type prod term -> (term -> term) -> term.
+  
+
+kind sealed-goal type.
+type nabla (term -> sealed-goal) -> sealed-goal.
+type seal goal -> sealed-goal.
+
+kind goal type.
+type goal list prop -> term -> term -> goal.
+
+type of term -> term -> prop.
+
+pred msolve o:list sealed-goal.
+  
+
+
+% ---- Builtin predicates ----
+
+% [lp.sig S T] Gives the type of a symbol
+external pred lp.sig i:symbol, o:term.
+
+% [lp.tc-instances L] Gives the list of type class instances
+external pred lp.tc-instances o:list symbol.
+
+% [lp.tc? S] Tells if S is a type class
+external pred lp.tc? i:symbol.
+
+% [lp.snf X SX] SX is the snf of X
+external pred lp.snf i:term, o:term.
+
+% [lp.eq_modulo X Y] X = Y upto rewrite
+external pred lp.eq_modulo i:term, i:term.
+
+% [lp.unif X Y] unify X with Y
+external pred lp.unif i:term, i:term.
+
+% [lp.term->string T S] Pretty prints a term T to the string S
+external pred lp.term->string i:term, o:string.
+
+% ---- Elpi predicates ----
+
+%  == Core builtins =====================================
+
+%  -- Logic --
+
+pred true.
+
+true.
+
+pred fail.
+
+pred false.
+
+external pred (=) o:A, o:A. % unification
+
+typeabbrev int (ctype "int").
+
+
+typeabbrev string (ctype "string").
+
+
+typeabbrev float (ctype "float").
+
+
+pred (;) o:prop, o:prop.
+
+(A ; _) :- A.
+
+(_ ; B) :- B.
+
+type (:-) prop -> prop -> prop.
+
+type (:-) prop -> list prop -> prop.
+
+type (,) variadic prop prop.
+
+type uvar A.
+
+type (as) A -> A -> A.
+
+type (=>) prop -> prop -> prop.
+
+type (=>) list prop -> prop -> prop.
+
+%  -- Control --
+
+external pred !. % The cut operator
+
+pred not i:prop.
+
+not X :- X, !, fail.
+
+not _.
+
+% [declare_constraint C Key1 Key2...] declares C blocked
+% on Key1 Key2 ... (variables, or lists thereof).
+external type declare_constraint variadic any prop.
+
+external pred print_constraints. % prints all constraints
+
+% [halt ...] halts the program and print the terms
+external type halt variadic any prop.
+
+pred stop.
+
+stop :- halt.
+
+%  -- Evaluation --
+
+% [calc Expr Out] unifies Out with the value of Expr. It can be used in
+% tandem with spilling, eg [f {calc (N + 1)}]
+external pred calc i:A, o:A.
+
+pred (is) o:A, i:A.
+
+X is Y :- calc Y X.
+
+type (-) A -> A -> A.
+
+type (i-) int -> int -> int.
+
+type (r-) float -> float -> float.
+
+type (+) int -> int -> int.
+
+type (+) float -> float -> float.
+
+type (i+) int -> int -> int.
+
+type (r+) float -> float -> float.
+
+type (*) int -> int -> int.
+
+type (*) float -> float -> float.
+
+type (/) float -> float -> float.
+
+type (mod) int -> int -> int.
+
+type (div) int -> int -> int.
+
+type (^) string -> string -> string.
+
+type (~) int -> int.
+
+type (~) float -> float.
+
+type (i~) int -> int.
+
+type (r~) float -> float.
+
+type abs int -> int.
+
+type abs float -> float.
+
+type iabs int -> int.
+
+type rabs float -> float.
+
+type max int -> int -> int.
+
+type max float -> float -> float.
+
+type min int -> int -> int.
+
+type min float -> float -> float.
+
+type sqrt float -> float.
+
+type sin float -> float.
+
+type cos float -> float.
+
+type arctan float -> float.
+
+type ln float -> float.
+
+type int_to_real int -> float.
+
+type floor float -> int.
+
+type ceil float -> int.
+
+type truncate float -> int.
+
+type size string -> int.
+
+type chr int -> string.
+
+type rhc string -> int.
+
+type string_to_int string -> int.
+
+type int_to_string int -> string.
+
+type substring string -> int -> int -> string.
+
+type real_to_string float -> string.
+
+%  -- Arithmetic tests --
+
+% [lt_ X Y] checks if X < Y. Works for string, int and float
+external pred lt_ i:A, i:A.
+
+% [gt_ X Y] checks if X > Y. Works for string, int and float
+external pred gt_ i:A, i:A.
+
+% [le_ X Y] checks if X =< Y. Works for string, int and float
+external pred le_ i:A, i:A.
+
+% [ge_ X Y] checks if X >= Y. Works for string, int and float
+external pred ge_ i:A, i:A.
+
+type (<), (>), (=<), (>=) A -> A -> prop.
+
+X  > Y  :- gt_ X Y.
+
+X  < Y  :- lt_ X Y.
+
+X  =< Y :- le_ X Y.
+
+X  >= Y :- ge_ X Y.
+
+type (i<), (i>), (i=<), (i>=) int -> int -> prop.
+
+X i< Y  :- lt_ X Y.
+
+X i> Y  :- gt_ X Y.
+
+X i=< Y :- le_ X Y.
+
+X i>= Y :- ge_ X Y.
+
+type (r<), (r>), (r=<), (r>=) float -> float -> prop.
+
+X r< Y  :- lt_ X Y.
+
+X r> Y  :- gt_ X Y.
+
+X r=< Y :- le_ X Y.
+
+X r>= Y :- ge_ X Y.
+
+type (s<), (s>), (s=<), (s>=) string -> string -> prop.
+
+X s< Y  :- lt_ X Y.
+
+X s> Y  :- gt_ X Y.
+
+X s=< Y :- le_ X Y.
+
+X s>= Y :- ge_ X Y.
+
+%  -- Standard data types (supported in the FFI) --
+
+kind list type -> type.
+
+type (::) X -> list X -> list X.
+
+type ([]) list X.
+
+% Boolean values: tt and ff since true and false are predicates
+kind bool type.
+type tt bool.
+type ff bool.
+
+% Pair: the constructor is pr, since ',' is for conjunction
+kind pair type -> type -> type.
+type pr A -> B -> pair A B.
+
+pred fst  i:pair A B, o:A.
+
+fst (pr A _) A.
+
+pred snd  i:pair A B, o:B.
+
+snd (pr _ B) B.
+
+% The option type (aka Maybe)
+kind option type -> type.
+type none option A.
+type some A -> option A.
+
+% Result of a comparison
+kind cmp type.
+type eq cmp.
+type lt cmp.
+type gt cmp.
+
+% Used in builtin variants that return Coq's error rather than failing
+kind diagnostic type.
+type ok diagnostic. % Success
+type error string -> diagnostic. % Failure
+
+%  == I/O builtins =====================================
+
+%  -- I/O --
+
+typeabbrev in_stream (ctype "in_stream").
+
+type std_in in_stream.
+
+typeabbrev out_stream (ctype "out_stream").
+
+type std_out out_stream.
+type std_err out_stream.
+
+% [open_in FileName InStream] opens FileName for input
+external pred open_in i:string, o:in_stream.
+
+% [open_out FileName OutStream] opens FileName for output
+external pred open_out i:string, o:out_stream.
+
+% [open_append FileName OutStream] opens FileName for output in append mode
+external pred open_append i:string, o:out_stream.
+
+% [close_in InStream] closes input stream InStream
+external pred close_in i:in_stream.
+
+% [close_out OutStream] closes output stream OutStream
+external pred close_out i:out_stream.
+
+% [output OutStream Data] writes Data to OutStream
+external pred output i:out_stream, i:string.
+
+% [flush OutStream] flush all output not yet finalized to OutStream
+external pred flush i:out_stream.
+
+% [input InStream Bytes Data] reads Bytes from InStream
+external pred input i:in_stream, i:int, o:string.
+
+% [input_line InStream Line] reads a full line from InStream
+external pred input_line i:in_stream, o:string.
+
+% [eof InStream] checks if no more data can be read from InStream
+external pred eof i:in_stream.
+
+%  -- System --
+
+% [gettimeofday T] sets T to the number of seconds elapsed since 1/1/1970
+external pred gettimeofday o:float.
+
+% [getenv VarName Value] Like Sys.getenv
+external pred getenv i:string, o:option string.
+
+% [system Command RetVal] executes Command and sets RetVal to the exit code
+external pred system i:string, o:int.
+
+%  -- Debugging --
+
+% [term_to_string T S] prints T to S
+external pred term_to_string i:any, o:string.
+
+% == Lambda Prolog builtins =====================================
+
+%  -- Extra I/O --
+
+% [open_string DataIn InStream] opens DataIn as an input stream
+external pred open_string i:string, o:in_stream.
+
+% [lookahead InStream NextChar] peeks one byte from InStream
+external pred lookahead i:in_stream, o:string.
+
+%  -- Hacks --
+
+% [string_to_term S T] parses a term T from S
+external pred string_to_term i:string, o:any.
+
+% [readterm InStream T] reads T from InStream, ends with \n
+external pred readterm i:in_stream, o:any.
+
+pred printterm i:out_stream, i:A.
+
+printterm S T :- term_to_string T T1, output S T1.
+
+pred read o:A.
+
+read S :- flush std_out, input_line std_in X, string_to_term X S.
+
+% == Elpi builtins =====================================
+
+% [dprint ...] prints raw terms (debugging)
+external type dprint variadic any prop.
+
+% [print ...] prints terms
+external type print variadic any prop.
+
+% Deprecated, use trace.counter
+pred counter i:string, o:int.
+counter C N :- trace.counter C N.
+
+% [quote_syntax FileName QueryText QuotedProgram QuotedQuery] quotes the
+% program from FileName and the QueryText. See elpi-quoted_syntax.elpi for
+% the syntax tree
+external pred quote_syntax i:string, i:string, o:list A, o:A.
+
+typeabbrev loc (ctype "Loc.t").
+
+
+% [loc.fields Loc File StartChar StopChar Line LineStartsAtChar] Decomposes
+% a loc into its fields
+external pred loc.fields i:loc, o:string, o:int, o:int, o:int, o:int.
+
+% == Regular Expressions =====================================
+
+% [rex.match Rex Subject] checks if Subject matches Rex. Matching is based
+% on OCaml's Str library
+external pred rex.match i:string, i:string.
+
+% [rex.replace Rex Replacement Subject Out] Out is obtained by replacing all
+% occurrences of Rex with Replacement in Subject. See also OCaml's
+% Str.global_replace
+external pred rex.replace i:string, i:string, i:string, o:string.
+
+% [rex.split Rex Subject Out] Out is obtained by splitting Subject at all
+% occurrences of Rex. See also OCaml's Str.split
+external pred rex.split i:string, i:string, o:list string.
+
+% Deprecated, use rex.match
+pred rex_match i:string, i:string.
+rex_match Rx S :- rex.match Rx S.
+
+% Deprecated, use rex.replace
+pred rex_replace i:string, i:string, i:string, o:string.
+rex_replace Rx R S O :- rex.replace Rx R S O.
+
+% Deprecated, use rex.split
+pred rex_split i:string, i:string, o:list string.
+rex_split Rx S L :- rex.split Rx S L.
+
+% == Elpi nonlogical builtins =====================================
+
+% Opaque ML data types
+kind ctyp type.
+type ctype string -> ctyp.
+
+% [var V ...] checks if the term V is a variable. When used with tree
+% arguments it relates an applied variable with its head and argument list.
+external type var any -> variadic any prop.
+
+% [prune V L] V is pruned to L (V is unified with a variable that only sees
+% the list of names L)
+external pred prune o:any, i:list any.
+
+% [distinct_names L] checks if L is a list of distinct names. If L is the
+% scope of a unification variable (its arguments, as per var predicate) then
+% distinct_names L checks that such variable is in the Miller pattern
+% fragment (L_\lambda)
+external pred distinct_names i:list any.
+
+% [same_var V1 V2] checks if the two terms V1 and V2 are the same variable,
+% ignoring the arguments of the variables
+external pred same_var i:A, i:A.
+
+% [same_term T1 T2] checks if the two terms T1 and T2 are syntactically
+% equal (no unification). It behaves differently than same_var since it
+% recursively compares the arguments of the variables
+external pred same_term i:A, i:A.
+
+
+% Infix notation for same_term
+pred (==) i:A, i:A.
+X == Y :- same_term X Y.
+
+
+% [cmp_term A B Cmp] Compares A and B. Only works if A and B are ground.
+external pred cmp_term i:any, i:any, o:cmp.
+
+% [name T ...] checks if T is a eigenvariable. When used with tree arguments
+% it relates an applied name with its head and argument list.
+external type name any -> variadic any prop.
+
+% [constant T ...] checks if T is a (global) constant.  When used with tree
+% arguments it relates an applied constant with its head and argument list.
+external type constant any -> variadic any prop.
+
+external pred names % generates the list of eigenvariable
+  o:list any. % list of eigenvariables in order of age (young first)
+  
+external pred occurs % checks if the atom occurs in the term
+  i:any, % an atom, that is a global constant or a bound name (aka eigenvariable)
+  i:any. % a term
+  
+% [closed_term T] unify T with a variable that has no eigenvariables in
+% scope
+external pred closed_term o:any.
+
+% [ground_term T] Checks if T contains unification variables
+external pred ground_term i:any.
+
+% [is_cdata T Ctype] checks if T is primitive of type Ctype, eg (ctype
+% "int")
+external pred is_cdata i:any, o:ctyp.
+
+pred primitive? i:A, i:string.
+
+primitive? X S :- is_cdata X (ctype S).
+
+% [new_int N] unifies N with a different int every time it is called. Values
+% of N are guaranteed to be incresing.
+external pred new_int o:int.
+
+% [findall_solution P L] finds all the solved instances of P and puts them
+% in L
+% in the order in which they are found. Instances can contain
+% eigenvariables
+% and unification variables.
+
+external pred findall_solutions i:prop, o:list prop.
+
+% Holds data across bracktracking; can only contain closed terms
+typeabbrev safe (ctype "safe").
+
+
+% [new_safe Safe] creates a safe: a store that persists across backtracking
+external pred new_safe o:safe.
+
+% [stash_in_safe Safe Data] stores Data in the Safe
+external pred stash_in_safe i:safe, i:A.
+
+% [open_safe Safe Data] retrieves the Data stored in Safe
+external pred open_safe i:safe, o:list A.
+
+
+% [if C T E] picks the first success of C then runs T (never E).
+% if C has no success it runs E.
+pred if i:prop, i:prop, i:prop.
+if B T _ :- B, !, T.
+if _ _ E :- E.
+
+% [if2 C1 B1 C2 B2 E] like if but with 2 then branches (and one else branch).
+pred if2 i:prop, i:prop, i:prop, i:prop, i:prop.
+if2 G1 P1 _  _  _ :- G1, !, P1.
+if2 _  _  G2 P2 _ :- G2, !, P2.
+if2 _  _  _  _  E :- !, E. 
+
+% [random.init Seed] Initialize OCaml's PRNG with the given Seed
+external pred random.init i:int.
+
+% [random.self_init] Initialize OCaml's PRNG with some seed
+external pred random.self_init .
+
+% [random.int Bound N] unifies N with a random int between 0 and Bound
+% (excluded)
+external pred random.int i:int, o:int.
+
+#line 0 "builtin_stdlib.elpi"
+% == stdlib =======================================================
+
+% Conventions:
+% - all predicates declare a mode with some input arguments, unless...
+% - predicates whose name ends with R are relations (work in any direction,
+%   that is all arguments are in output mode)
+% - predicates whose name ends with ! do contain a cut and generate only the
+%   first result
+% - all errors given by this library end up calling fatal-error[-w-data],
+%   override it in order to handle them differently
+% - all debug prints by this library end up calling debug-print, override it
+%   in order to handle them differently
+
+namespace std {
+
+pred fatal-error i:string.
+:name "default-fatal-error"
+fatal-error Msg :- halt Msg.
+
+pred fatal-error-w-data i:string, i:A.
+:name "default-fatal-error-w-data"
+fatal-error-w-data Msg Data :- halt Msg ":" Data.
+
+pred debug-print i:string, i:A.
+:name "default-debug-print"
+debug-print Msg Data :- print Msg Data.
+
+%  -- Errors, Debugging, Hacks --
+
+pred ignore-failure! i:prop.
+ignore-failure! P :- P, !.
+ignore-failure! _.
+
+% [assert! C M] takes the first success of C or fails with message M 
+pred assert! i:prop, i:string.
+assert! Cond Msg :- (Cond ; fatal-error-w-data Msg Cond), !.
+
+% [assert-ok! C M] like assert! but the last argument of the predicate must
+% be a diagnostic that is printed after M in case it is not ok
+pred assert-ok! i:(diagnostic -> prop), i:string.
+assert-ok! Cond Msg :- Cond Diagnostic, !, (Diagnostic = ok ; Diagnostic = error S, fatal-error-w-data Msg S), !.
+assert-ok! _ Msg :- fatal-error-w-data Msg "no diagnostic returned".
+
+% [spy P] traces the call to P, printing all success and the final failure
+pred spy i:prop.
+spy P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
+         debug-print "----<<---- enter: " P,
+         P,
+         debug-print "---->>---- exit: " P.
+spy P :- debug-print "---->>---- fail: " P, fail.
+
+% [spy! P] traces the first call to P without leaving a choice point
+pred spy! i:prop.
+spy! P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
+         debug-print "----<<---- enter: " P,
+         P,
+         debug-print "---->>---- exit: " P, !.
+spy! P :- debug-print "---->>---- fail: " P, fail.
+
+% to silence the type checker
+pred unsafe-cast o:A, o:B.
+unsafe-cast X X.
+
+% -- List processing --
+
+pred length i:list A, o:int.
+length [_|L] N :- length L N1, N is N1 + 1.
+length []    0.
+
+pred rev i:list A, o:list A.
+rev L RL  :- rev.aux L []  RL.
+rev.aux [X|XS] ACC R :- rev.aux XS [X|ACC] R.
+rev.aux [] L L.
+
+pred last i:list A, o:A.
+last [] _ :- fatal-error "last on empty list".
+last [X] X :- !.
+last [_|XS] R :- last XS R.
+
+pred append i:list A, i:list A, o:list A.
+append [X|XS] L [X|L1] :- append XS L L1 .
+append [] L L .
+
+pred appendR o:list A, o:list A, o:list A.
+appendR [X|XS] L [X|L1] :- appendR XS L L1 .
+appendR [] L L .
+
+pred take i:int, i:list A, o:list A.
+take 0 _ [] :- !.
+take N [X|XS] [X|L] :- !, N1 is N - 1, take N1 XS L.
+take _ _ _ :- fatal-error "take run out of list items".
+
+pred take-last i:int, i:list A, o:list A.
+take-last N L R :-
+  length L M,
+  D is M - N,
+  drop D L R.
+
+pred drop i:int, i:list A, o:list A.
+drop 0 L L :- !.
+drop N [_|XS] L :- !, N1 is N - 1, drop N1 XS L.
+drop _ _ _ :- fatal-error "drop run out of list items".
+
+pred drop-last i:int, i:list A, o:list A.
+drop-last N L R :-
+  length L M, I is M - N, take I L R.
+
+pred split-at i:int, i:list A, o:list A, o:list A.
+split-at 0 L [] L :- !.
+split-at N [X|XS] [X|LN] LM :- !, N1 is N - 1, split-at N1 XS LN LM.
+split-at _ _ _ _ :- fatal-error "split-at run out of list items".
+
+pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.
+fold [] A _ A.
+fold [X|XS] A F R :- F X A A1, fold XS A1 F R.
+
+pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.
+fold2 [] [_|_] _ _ _ :- fatal-error "fold2 on lists of different length".
+fold2 [_|_] [] _ _ _ :- fatal-error "fold2 on lists of different length".
+fold2 [] [] A _ A.
+fold2 [X|XS] [Y|YS] A F R :- F X Y A A1, fold2 XS YS A1 F R.
+
+pred map i:list A, i:(A -> B -> prop), o:list B.
+map [] _ [].
+map [X|XS] F [Y|YS] :- F X Y, map XS F YS.
+
+pred map-i i:list A, i:(int -> A -> B -> prop), o:list B.
+map-i L F R :- map-i.aux L 0 F R.
+map-i.aux [] _ _ [].
+map-i.aux [X|XS] N F [Y|YS] :- F N X Y, M is N + 1, map-i.aux XS M F YS.
+
+pred map-filter i:list A, i:(A -> B -> prop), o:list B.
+map-filter [] _ [].
+map-filter [X|XS] F [Y|YS] :- F X Y, !, map-filter XS F YS.
+map-filter [_|XS] F YS :- map-filter XS F YS.
+
+:index(1 1)
+pred map2 i:list A, i:list B, i:(A -> B -> C -> prop), o:list C.
+map2 [] [_|_] _ _ :- fatal-error "map2 on lists of different length".
+map2 [_|_] [] _ _ :- fatal-error "map2 on lists of different length".
+map2 [] [] _ [].
+map2 [X|XS] [Y|YS] F [Z|ZS] :- F X Y Z, map2 XS YS F ZS.
+
+pred map2-filter i:list A, i:list B, i:(A -> B -> C -> prop), o:list C.
+map2-filter [] [_|_] _ _ :- fatal-error "map2-filter on lists of different length".
+map2-filter [_|_] [] _ _ :- fatal-error "map2-filter on lists of different length".
+map2-filter [] [] _ [].
+map2-filter [X|XS] [Y|YS] F [Z|ZS] :- F X Y Z, !, map2-filter XS YS F ZS.
+map2-filter [_|XS] [_|YS] F ZS :- map2-filter XS YS F ZS.
+
+pred map-ok i:list A, i:(A -> B -> diagnostic -> prop), o:list A, o:diagnostic.
+map-ok [X|L] P [Y|YS] S :- P X Y S0, if (S0 = ok) (map-ok L P YS S) (S = S0).
+map-ok [] _ [] ok.
+
+pred fold-map i:list A, i:B, i:(A -> B -> C -> B -> prop), o:list C, o:B.
+fold-map [] A _ [] A.
+fold-map [X|XS] A F [Y|YS] A2 :- F X A Y A1, fold-map XS A1 F YS A2.
+
+pred omap i:option A, i:(A -> B -> prop), o:option B.
+omap none _ none.
+omap (some X) F (some Y) :- F X Y.
+
+% [nth N L X] picks in X the N-th element of L (L must be of length > N)
+pred nth i:int, i:list A, o:A.
+nth 0 [X|_ ] R :- !, X = R.
+nth N [_|XS] R :- N > 0, !, N1 is N - 1, nth N1 XS R.
+nth N _ _ :- N < 0, !, fatal-error "nth got a negative index".
+nth _ _ _ :- fatal-error "nth run out of list items".
+
+% [lookup L K V] sees L as a map from K to V
+pred lookup i:list (pair A B), i:A, o:B.
+lookup [pr X Y|_] X Y.
+lookup [_|LS]       X Y :- lookup LS X Y.
+
+% [lookup! L K V] sees L as a map from K to V, stops at the first binding
+pred lookup! i:list (pair A B), i:A, o:B.
+lookup! [pr X Y|_] X Y :- !.
+lookup! [_|LS]       X Y :- lookup! LS X Y.
+
+% [mem! L X] succeeds once if X occurs inside L 
+pred mem! i:list A, o:A.
+mem! [X|_] X :- !.
+mem! [_|L] X :- mem! L X.
+
+% [mem L X] succeeds every time if X occurs inside L 
+pred mem i:list A, o:A.
+mem [X|_] X.
+mem [_|L] X :- mem L X.
+
+pred exists i:list A, i:(A -> prop).
+exists [X|_] P :- P X.
+exists [_|L] P :- exists L P.
+
+pred exists2 i:list A, i:list B, i:(A -> B -> prop).
+exists2 [] [_|_] _ :- fatal-error "exists2 on lists of different length".
+exists2 [_|_] [] _ :- fatal-error "exists2 on lists of different length".
+exists2 [X|_] [Y|_] P :- P X Y.
+exists2 [_|L] [_|M] P :- exists2 L M P.
+
+pred forall i:list A, i:(A -> prop).
+forall [] _.
+forall [X|L] P :- P X, forall L P.
+
+pred forall-ok i:list A, i:(A -> diagnostic -> prop), o:diagnostic.
+forall-ok [X|L] P S :- P X S0, if (S0 = ok) (forall-ok L P S) (S = S0).
+forall-ok [] _ ok.
+
+pred forall2 i:list A, i:list B, i:(A -> B -> prop).
+forall2 [] [_|_] _ :- fatal-error "forall2 on lists of different length".
+forall2 [_|_] [] _ :- fatal-error "forall2 on lists of different length".
+forall2 [X|XS] [Y|YS] P :- P X Y, forall2 XS YS P.
+forall2 [] [] _.
+
+pred filter i:list A, i:(A -> prop), o:list A.
+filter []    _ [].
+filter [X|L] P R :- if (P X) (R = X :: L1) (R = L1), filter L P L1.
+
+pred zip i:list A, i:list B, o:list (pair A B).
+zip [_|_] [] _ :- fatal-error "zip on lists of different length".
+zip [] [_|_] _ :- fatal-error "zip on lists of different length".
+zip [X|LX] [Y|LY] [pr X Y|LR] :- zip LX LY LR.
+zip [] [] [].
+
+pred unzip i:list (pair A B), o:list A, o:list B.
+unzip [] [] [].
+unzip [pr X Y|L] [X|LX] [Y|LY] :- unzip L LX LY.
+
+pred flatten i:list (list A), o:list A.
+flatten [X|LS] R :- flatten LS LS', append X LS' R.
+flatten []     [].
+
+pred null i:list A.
+null [].
+
+pred iota i:int, o:list int.
+iota N L :- iota.aux 0 N L.
+iota.aux X X [] :- !.
+iota.aux N X [N|R] :- M is N + 1, iota.aux M X R.
+
+% [intersperse X L R] R is [L0, X, ..., X, LN]
+:index(_ 1)
+pred intersperse i:A, i:list A, o:list A.
+intersperse _ [] [].
+intersperse _ [X] [X] :- !.
+intersperse Sep [X|XS] [X,Sep|YS] :- intersperse Sep XS YS.
+
+%  -- Misc --
+
+pred flip i:(A -> B -> prop), i:B, i:A.
+flip P X Y :- P Y X.
+
+pred time i:prop, o:float.
+time P T :- gettimeofday Before, P, gettimeofday After, T is After - Before.
+
+pred do! i:list prop.
+do! [].
+do! [P|PS] :- P, !, do! PS.
+
+:index(_ 1)
+pred do-ok! o:diagnostic, i:list (diagnostic -> prop).
+do-ok! ok [].
+do-ok! S [P|PS] :- P S0, !, if (S0 = ok) (do-ok! S PS) (S = S0).
+
+pred lift-ok i:prop, i:string, o:diagnostic.
+lift-ok P Msg R :- (P, R = ok; R = error Msg).
+
+pred spy-do! i:list prop.
+spy-do! L :- map L (x\y\y = spy x) L1, do! L1.
+
+pred while-ok-do! i:diagnostic, i:list (diagnostic -> prop), o:diagnostic.
+while-ok-do! (error _ as E) _ E.
+while-ok-do! ok [] ok.
+while-ok-do! ok [P|PS] R :- P C, !, while-ok-do! C PS R.
+
+pred any->string i:A, o:string.
+any->string X Y :- term_to_string X Y.
+
+pred max i:A, i:A, o:A.
+max N M N :- N >= M, !.
+max _ M M.
+
+% [findall P L] L is the list [P1,P2,P3..] where each Pi is a solution to P.
+pred findall i:prop, o:list prop.
+findall P L :- findall_solutions P L.
+
+}
+
+% [std.string.concat Separator Items Result] concatenates Items
+% interspersing Separator
+external pred std.string.concat i:string, i:list string, o:string.
+
+% CAVEAT: the type parameter of std.string.map must be a closed term
+
+kind std.string.map type -> type.
+
+% [std.string.map.empty M] The empty map
+external pred std.string.map.empty o:std.string.map A.
+
+% [std.string.map.mem S M] Checks if S is bound in M
+external pred std.string.map.mem i:string, i:std.string.map A.
+
+% [std.string.map.add S V M M1] M1 is M where V is bound to S
+external pred std.string.map.add i:string, i:A, i:std.string.map A, 
+                                 o:std.string.map A.
+
+% [std.string.map.remove S M M1] M1 is M where S is unbound
+external pred std.string.map.remove i:string, i:std.string.map A, 
+                                    o:std.string.map A.
+
+% [std.string.map.find S M V] V is the binding of S in M
+external pred std.string.map.find i:string, i:std.string.map A, o:A.
+
+% [std.string.map.bindings M L] L is M transformed into an associative list
+external pred std.string.map.bindings i:std.string.map A, 
+                                      o:list (pair string A).
+
+% CAVEAT: the type parameter of std.int.map must be a closed term
+
+kind std.int.map type -> type.
+
+% [std.int.map.empty M] The empty map
+external pred std.int.map.empty o:std.int.map A.
+
+% [std.int.map.mem S M] Checks if S is bound in M
+external pred std.int.map.mem i:int, i:std.int.map A.
+
+% [std.int.map.add S V M M1] M1 is M where V is bound to S
+external pred std.int.map.add i:int, i:A, i:std.int.map A, 
+                              o:std.int.map A.
+
+% [std.int.map.remove S M M1] M1 is M where S is unbound
+external pred std.int.map.remove i:int, i:std.int.map A, o:std.int.map A.
+
+% [std.int.map.find S M V] V is the binding of S in M
+external pred std.int.map.find i:int, i:std.int.map A, o:A.
+
+% [std.int.map.bindings M L] L is M transformed into an associative list
+external pred std.int.map.bindings i:std.int.map A, o:list (pair int A).
+
+% CAVEAT: the type parameter of std.loc.map must be a closed term
+
+kind std.loc.map type -> type.
+
+% [std.loc.map.empty M] The empty map
+external pred std.loc.map.empty o:std.loc.map A.
+
+% [std.loc.map.mem S M] Checks if S is bound in M
+external pred std.loc.map.mem i:loc, i:std.loc.map A.
+
+% [std.loc.map.add S V M M1] M1 is M where V is bound to S
+external pred std.loc.map.add i:loc, i:A, i:std.loc.map A, 
+                              o:std.loc.map A.
+
+% [std.loc.map.remove S M M1] M1 is M where S is unbound
+external pred std.loc.map.remove i:loc, i:std.loc.map A, o:std.loc.map A.
+
+% [std.loc.map.find S M V] V is the binding of S in M
+external pred std.loc.map.find i:loc, i:std.loc.map A, o:A.
+
+% [std.loc.map.bindings M L] L is M transformed into an associative list
+external pred std.loc.map.bindings i:std.loc.map A, o:list (pair loc A).
+
+kind std.string.set type.
+
+% [std.string.set.empty A] The empty set
+external pred std.string.set.empty o:std.string.set.
+
+% [std.string.set.mem Elem A] Checks if Elem is in a
+external pred std.string.set.mem i:string, i:std.string.set.
+
+% [std.string.set.add Elem A B] B is A union {Elem}
+external pred std.string.set.add i:string, i:std.string.set, 
+                                 o:std.string.set.
+
+% [std.string.set.remove Elem A B] B is A \ {Elem}
+external pred std.string.set.remove i:string, i:std.string.set, 
+                                    o:std.string.set.
+
+% [std.string.set.union A B X] X is A union B
+external pred std.string.set.union i:std.string.set, i:std.string.set, 
+                                   o:std.string.set.
+
+% [std.string.set.inter A B X] X is A intersection B
+external pred std.string.set.inter i:std.string.set, i:std.string.set, 
+                                   o:std.string.set.
+
+% [std.string.set.diff A B X] X is A \ B
+external pred std.string.set.diff i:std.string.set, i:std.string.set, 
+                                  o:std.string.set.
+
+% [std.string.set.equal A B] tests A and B for equality
+external pred std.string.set.equal i:std.string.set, i:std.string.set.
+
+% [std.string.set.subset A B] tests if A is a subset of B
+external pred std.string.set.subset i:std.string.set, i:std.string.set.
+
+% [std.string.set.elements M L] L is M transformed into list
+external pred std.string.set.elements i:std.string.set, o:list string.
+
+% [std.string.set.cardinal M N] N is the number of elements of M
+external pred std.string.set.cardinal i:std.string.set, o:int.
+
+kind std.int.set type.
+
+% [std.int.set.empty A] The empty set
+external pred std.int.set.empty o:std.int.set.
+
+% [std.int.set.mem Elem A] Checks if Elem is in a
+external pred std.int.set.mem i:int, i:std.int.set.
+
+% [std.int.set.add Elem A B] B is A union {Elem}
+external pred std.int.set.add i:int, i:std.int.set, o:std.int.set.
+
+% [std.int.set.remove Elem A B] B is A \ {Elem}
+external pred std.int.set.remove i:int, i:std.int.set, o:std.int.set.
+
+% [std.int.set.union A B X] X is A union B
+external pred std.int.set.union i:std.int.set, i:std.int.set, 
+                                o:std.int.set.
+
+% [std.int.set.inter A B X] X is A intersection B
+external pred std.int.set.inter i:std.int.set, i:std.int.set, 
+                                o:std.int.set.
+
+% [std.int.set.diff A B X] X is A \ B
+external pred std.int.set.diff i:std.int.set, i:std.int.set, 
+                               o:std.int.set.
+
+% [std.int.set.equal A B] tests A and B for equality
+external pred std.int.set.equal i:std.int.set, i:std.int.set.
+
+% [std.int.set.subset A B] tests if A is a subset of B
+external pred std.int.set.subset i:std.int.set, i:std.int.set.
+
+% [std.int.set.elements M L] L is M transformed into list
+external pred std.int.set.elements i:std.int.set, o:list int.
+
+% [std.int.set.cardinal M N] N is the number of elements of M
+external pred std.int.set.cardinal i:std.int.set, o:int.
+
+kind std.loc.set type.
+
+% [std.loc.set.empty A] The empty set
+external pred std.loc.set.empty o:std.loc.set.
+
+% [std.loc.set.mem Elem A] Checks if Elem is in a
+external pred std.loc.set.mem i:loc, i:std.loc.set.
+
+% [std.loc.set.add Elem A B] B is A union {Elem}
+external pred std.loc.set.add i:loc, i:std.loc.set, o:std.loc.set.
+
+% [std.loc.set.remove Elem A B] B is A \ {Elem}
+external pred std.loc.set.remove i:loc, i:std.loc.set, o:std.loc.set.
+
+% [std.loc.set.union A B X] X is A union B
+external pred std.loc.set.union i:std.loc.set, i:std.loc.set, 
+                                o:std.loc.set.
+
+% [std.loc.set.inter A B X] X is A intersection B
+external pred std.loc.set.inter i:std.loc.set, i:std.loc.set, 
+                                o:std.loc.set.
+
+% [std.loc.set.diff A B X] X is A \ B
+external pred std.loc.set.diff i:std.loc.set, i:std.loc.set, 
+                               o:std.loc.set.
+
+% [std.loc.set.equal A B] tests A and B for equality
+external pred std.loc.set.equal i:std.loc.set, i:std.loc.set.
+
+% [std.loc.set.subset A B] tests if A is a subset of B
+external pred std.loc.set.subset i:std.loc.set, i:std.loc.set.
+
+% [std.loc.set.elements M L] L is M transformed into list
+external pred std.loc.set.elements i:std.loc.set, o:list loc.
+
+% [std.loc.set.cardinal M N] N is the number of elements of M
+external pred std.loc.set.cardinal i:std.loc.set, o:int.
+
+#line 0 "builtin_map.elpi"
+kind std.map type -> type -> type.
+type std.map std.map.private.map K V -> (K -> K -> cmp -> prop) -> std.map K V.
+
+namespace std.map {
+
+% [make Eq Ltn M] builds an empty map M where keys are compared using Eq and Ltn
+pred make i:(K -> K -> cmp -> prop), o:std.map K V.
+make Cmp (std.map private.empty Cmp).
+
+% [find K M V] looks in M for the value V associated to K
+pred find i:K, i:std.map K V, o:V.
+find K (std.map M Cmp) V :- private.find M Cmp K V.
+
+% [add K V M M1] M1 is M where K is bound to V
+pred add i:K, i:V, i:std.map K V, o:std.map K V.
+add K V (std.map M Cmp) (std.map M1 Cmp) :- private.add M Cmp K V M1.
+
+% [remove K M M1] M1 is M where K is unbound
+pred remove i:K, i:std.map K V, o:std.map K V.
+remove K (std.map M Cmp) (std.map M1 Cmp) :- private.remove M Cmp K M1.
+
+% [bindings M L] L is the key-value pairs in increasing order
+pred bindings i:std.map K V, o:list (pair K V).
+bindings (std.map M _) L :- private.bindings M [] L.
+
+namespace private {
+
+% Taken from OCaml's map.ml
+kind map type -> type -> type.
+type empty map K V.
+type node map K V -> K -> V -> map K V -> int -> map K V.
+
+pred height i:map K V, o:int.
+height empty 0.
+height (node _ _ _ _ H) H.
+
+pred create i:map K V, i:K, i:V, i:map K V, o:map K V.
+create L K V R (node L K V R H) :- H is {std.max {height L} {height R}} + 1.
+
+pred bal i:map K V, i:K, i:V, i:map K V, o:map K V.
+bal L K V R T :-
+  height L HL,
+  height R HR,
+  HL2 is HL + 2,
+  HR2 is HR + 2,
+  bal.aux HL HR HL2 HR2 L K V R T.
+
+bal.aux HL _ _ HR2 (node LL LV LD LR _) X D R T :-
+  HL > HR2, {height LL} >= {height LR}, !,
+  create LL LV LD {create LR X D R} T.
+bal.aux HL _ _ HR2 (node LL LV LD (node LRL LRV LRD LRR _) _) X D R T :-
+  HL > HR2, !,
+  create {create LL LV LD LRL} LRV LRD {create LRR X D R} T.
+bal.aux _ HR HL2 _ L X D (node RL RV RD RR _) T :-
+  HR > HL2, {height RR} >= {height RL}, !,
+  create {create L X D RL} RV RD RR T.
+bal.aux _ HR HL2 _ L X D (node (node RLL RLV RLD RLR _) RV RD RR _) T :-
+  HR > HL2, !,
+  create {create L X D RLL} RLV RLD {create RLR RV RD RR} T.
+bal.aux _ _ _ _ L K V R T :- create L K V R T.
+
+pred add i:map K V, i:(K -> K -> cmp -> prop), i:K, i:V, o:map K V.
+add empty _ K V T :- create empty K V empty T.
+add (node _ X _ _ _ as M) Cmp X1 XD M1 :- Cmp X1 X E, add.aux E M Cmp X1 XD M1.
+add.aux eq (node L _ _ R H) _   X XD T :- T = node L X XD R H. 
+add.aux lt (node L V D R _) Cmp X XD T :- bal {add L Cmp X XD} V D R T.
+add.aux gt (node L V D R _) Cmp X XD T :- bal L V D {add R Cmp X XD} T.
+
+pred find i:map K V, i:(K -> K -> cmp -> prop), i:K, o:V.
+find (node L K1 V1 R _) Cmp K V :- Cmp K K1 E, find.aux E Cmp L R V1 K V.
+find.aux eq _   _ _ V _ V.
+find.aux lt Cmp L _ _ K V :- find L Cmp K V.
+find.aux gt Cmp _ R _ K V :- find R Cmp K V.
+
+pred remove-min-binding i:map K V, o:map K V.
+remove-min-binding (node empty _ _ R _) R :- !.
+remove-min-binding (node L V D R _) X :- bal {remove-min-binding L} V D R X.
+
+pred min-binding i:map K V, o:K, o:V.
+min-binding (node empty V D _ _) V D :- !.
+min-binding (node L _ _ _ _) V D :- min-binding L V D.
+
+pred merge i:map K V, i:map K V, o:map K V.
+merge empty X X :- !.
+merge X empty X :- !.
+merge M1 M2 R :-
+  min-binding M2 X D,
+  bal M1 X D {remove-min-binding M2} R.
+
+pred remove i:map K V, i:(K -> K -> cmp -> prop), i:K, o:map K V.
+remove empty _ _ empty :- !.
+remove (node L V D R _) Cmp X M :- Cmp X V E, remove.aux E Cmp L R V D X M.
+remove.aux eq _   L R _ _ _ M :- merge L R M.
+remove.aux lt Cmp L R V D X M :- bal {remove L Cmp X} V D R M.
+remove.aux gt Cmp L R V D X M :- bal L V D {remove R Cmp X} M.
+
+pred bindings i:map K V, i:list (pair K V), o:list (pair K V).
+bindings empty X X.
+bindings (node L V D R _) X X1 :-
+  bindings L [pr V D|{bindings R X}] X1.
+
+
+} % std.map.private
+} % std.map
+
+
+#line 0 "builtin_set.elpi"
+kind std.set type -> type.
+type std.set std.set.private.set E -> (E -> E -> cmp -> prop) -> std.set E.
+
+namespace std.set {
+
+% [make Eq Ltn M] builds an empty set M where keys are compared using Eq and Ltn
+pred make i:(E -> E -> cmp -> prop), o:std.set E.
+make Cmp (std.set private.empty Cmp).
+
+% [mem E M] looks if E is in M
+pred mem i:E, i:std.set E.
+mem E (std.set M Cmp):- private.mem M Cmp E.
+
+% [add E M M1] M1 is M + {E}
+pred add i:E, i:std.set E, o:std.set E.
+add E (std.set M Cmp) (std.set M1 Cmp) :- private.add M Cmp E M1.
+
+% [remove E M M1] M1 is M - {E}
+pred remove i:E, i:std.set E, o:std.set E.
+remove E (std.set M Cmp) (std.set M1 Cmp) :- private.remove M Cmp E M1.
+
+% [cardinal S N] N is the number of elements of S
+pred cardinal i:std.set E, o:int.
+cardinal (std.set M _) N :- private.cardinal M N.
+
+pred elements i:std.set E, o:list E.
+elements (std.set M _) L :- private.elements M [] L.
+
+namespace private {
+
+% Taken from OCaml's set.ml
+kind set type -> type.
+type empty set E.
+type node set E -> E -> set E -> int -> set E.
+
+pred height i:set E, o:int.
+height empty 0.
+height (node _ _ _ H) H.
+
+pred create i:set E, i:E, i:set E, o:set E.
+create L E R (node L E R H) :- H is {std.max {height L} {height R}} + 1.
+
+pred bal i:set E, i:E, i:set E, o:set E.
+bal L E R T :-
+  height L HL,
+  height R HR,
+  HL2 is HL + 2,
+  HR2 is HR + 2,
+  bal.aux HL HR HL2 HR2 L E R T.
+
+bal.aux HL _ _ HR2 (node LL LV LR _) X R T :-
+  HL > HR2, {height LL} >= {height LR}, !,
+  create LL LV {create LR X R} T.
+bal.aux HL _ _ HR2 (node LL LV (node LRL LRV LRR _) _) X R T :-
+  HL > HR2, !,
+  create {create LL LV LRL} LRV {create LRR X R} T.
+bal.aux _ HR HL2 _ L X (node RL RV RR _) T :-
+  HR > HL2, {height RR} >= {height RL}, !,
+  create {create L X RL} RV RR T.
+bal.aux _ HR HL2 _ L X (node (node RLL RLV RLR _) RV RR _) T :-
+  HR > HL2, !,
+  create {create L X RLL} RLV {create RLR RV RR} T.
+bal.aux _ _ _ _ L E R T :- create L E R T.
+
+pred add i:set E, i:(E -> E -> cmp -> prop), i:E, o:set E.
+add empty _ E T :- create empty E empty T.
+add (node L X R H) Cmp X1 S :- Cmp X1 X E, add.aux E Cmp L R X X1 H S.
+add.aux eq _ L R X _ H (node L X R H).
+add.aux lt Cmp L R E X _ T :- bal {add L Cmp X} E R T.
+add.aux gt Cmp L R E X _ T :- bal L E {add R Cmp X} T.
+
+pred mem i:set E, i:(E -> E -> cmp -> prop), i:E.
+mem (node L K R _) Cmp E :- Cmp E K O, mem.aux O Cmp L R E.
+mem.aux eq _ _ _ _.
+mem.aux lt Cmp L _ E :- mem L Cmp E.
+mem.aux gt Cmp _ R E :- mem R Cmp E.
+
+pred remove-min-binding i:set E, o:set E.
+remove-min-binding (node empty _ R _) R :- !.
+remove-min-binding (node L E R _) X :- bal {remove-min-binding L} E R X.
+
+pred min-binding i:set E, o:E.
+min-binding (node empty E _ _) E :- !.
+min-binding (node L _ _ _) E :- min-binding L E.
+
+pred merge i:set E, i:set E, o:set E.
+merge empty X X :- !.
+merge X empty X :- !.
+merge M1 M2 R :-
+  min-binding M2 X,
+  bal M1 X {remove-min-binding M2} R.
+
+pred remove i:set E, i:(E -> E -> cmp -> prop), i:E, o:set E.
+remove empty _ _ empty.
+remove (node L E R _) Cmp X M :- Cmp X E O, remove.aux O Cmp L R E X M.
+remove.aux eq _   L R _ _ M :- merge L R M.
+remove.aux lt Cmp L R E X M :- bal {remove L Cmp X} E R M.
+remove.aux gt Cmp L R E X M :- bal L E {remove R Cmp X} M.
+
+pred cardinal i:set E, o:int.
+cardinal empty 0.
+cardinal (node L _ R _) N :- N is {cardinal L} + 1 + {cardinal R}.
+
+pred elements i:set E, i:list E, o:list E.
+elements empty X X.
+elements (node L E R _) Acc X :-
+  elements L [E|{elements R Acc}] X.
+
+} % std.set.private
+} % std.set
+
+
+% == Elpi runtime builtins =====================================
+
+% [trace.counter Name Value] reads the Value of a trace point Name
+external pred trace.counter i:string, o:int.
+
+% [gc.get MinorHeapSize MajorHeapIncrement SpaceOverhead Verbose MaxOverhead
+% StackLimit AllocationPolicy WindowSize] Reads the current settings of the
+% garbage collector. See also OCaml's Gc.control type documentation.
+external pred gc.get o:int, o:int, o:int, o:int, o:int, o:int, o:int, 
+                     o:int.
+
+% [gc.set MinorHeapSize MajorHeapIncrement SpaceOverhead Verbose MaxOverhead
+% StackLimit AllocationPolicy WindowSize] Writes the current settings of the
+% garbage collector. Any parameter left unspecificed (eg _) is not changed.
+% See also OCaml's Gc.control type documentation.
+external pred gc.set i:int, i:int, i:int, i:int, i:int, i:int, i:int, 
+                     i:int.
+
+% [gc.minor] See OCaml's Gc.minor documentation.
+external pred gc.minor .
+
+% [gc.major] See OCaml's Gc.major documentation.
+external pred gc.major .
+
+% [gc.full] See OCaml's Gc.full_major documentation.
+external pred gc.full .
+
+% [gc.compact] See OCaml's Gc.compact documentation.
+external pred gc.compact .
+
+% [gc.stat MinorWords PromotedWords MajorWords MinorCollections
+% MajorCollections HeapWords HeapChunks LiveWords LiveBlocks FreeWords
+% FreeBlocks LargestFree Fragments Compactions TopHeapWords StackSize] See
+% OCaml's Gc.stat documentation.
+external pred gc.stat o:float, o:float, o:float, o:int, o:int, o:int, 
+                      o:int, o:int, o:int, o:int, o:int, o:int, o:int, 
+                      o:int, o:int, o:int.
+
+% [gc.quick-stat MinorWords PromotedWords MajorWords MinorCollections
+% MajorCollections HeapWords HeapChunks Compactions TopHeapWords StackSize]
+% See OCaml's Gc.quick_stat documentation.
+external pred gc.quick-stat o:float, o:float, o:float, o:int, o:int, 
+                            o:int, o:int, o:int, o:int, o:int.
+
+
+
+
diff --git a/lambdapi.opam b/lambdapi.opam
index 829e849c9..0bb6353fa 100644
--- a/lambdapi.opam
+++ b/lambdapi.opam
@@ -62,6 +62,7 @@ depends: [
   "cmdliner" {>= "1.1.0"}
   "stdlib-shims" {>= "0.1.0"}
   "odoc" {with-doc}
+  "elpi" { >= "1.16.6" & < "1.17.0" }
 ]
 build: [
   ["dune" "subst"] {dev}
diff --git a/out/Coq__Arith__Arith__base.dk.gz b/out/Coq__Arith__Arith__base.dk.gz
new file mode 100644
index 000000000..c477060be
Binary files /dev/null and b/out/Coq__Arith__Arith__base.dk.gz differ
diff --git a/out/Coq__Arith__Between.dk.gz b/out/Coq__Arith__Between.dk.gz
new file mode 100644
index 000000000..32a04f860
Binary files /dev/null and b/out/Coq__Arith__Between.dk.gz differ
diff --git a/out/Coq__Arith__Compare__dec.dk.gz b/out/Coq__Arith__Compare__dec.dk.gz
new file mode 100644
index 000000000..c759d8030
Binary files /dev/null and b/out/Coq__Arith__Compare__dec.dk.gz differ
diff --git a/out/Coq__Arith__EqNat.dk.gz b/out/Coq__Arith__EqNat.dk.gz
new file mode 100644
index 000000000..77abe4a9d
Binary files /dev/null and b/out/Coq__Arith__EqNat.dk.gz differ
diff --git a/out/Coq__Arith__Factorial.dk.gz b/out/Coq__Arith__Factorial.dk.gz
new file mode 100644
index 000000000..1d691cb7f
Binary files /dev/null and b/out/Coq__Arith__Factorial.dk.gz differ
diff --git a/out/Coq__Arith__Gt.dk.gz b/out/Coq__Arith__Gt.dk.gz
new file mode 100644
index 000000000..5182b6957
Binary files /dev/null and b/out/Coq__Arith__Gt.dk.gz differ
diff --git a/out/Coq__Arith__Le.dk.gz b/out/Coq__Arith__Le.dk.gz
new file mode 100644
index 000000000..7767122f7
Binary files /dev/null and b/out/Coq__Arith__Le.dk.gz differ
diff --git a/out/Coq__Arith__Lt.dk.gz b/out/Coq__Arith__Lt.dk.gz
new file mode 100644
index 000000000..11c83dee2
Binary files /dev/null and b/out/Coq__Arith__Lt.dk.gz differ
diff --git a/out/Coq__Arith__Minus.dk.gz b/out/Coq__Arith__Minus.dk.gz
new file mode 100644
index 000000000..d2b3dd585
Binary files /dev/null and b/out/Coq__Arith__Minus.dk.gz differ
diff --git a/out/Coq__Arith__Mult.dk.gz b/out/Coq__Arith__Mult.dk.gz
new file mode 100644
index 000000000..84ea77ab9
Binary files /dev/null and b/out/Coq__Arith__Mult.dk.gz differ
diff --git a/out/Coq__Arith__PeanoNat.dk.gz b/out/Coq__Arith__PeanoNat.dk.gz
new file mode 100644
index 000000000..6b43f3b51
Binary files /dev/null and b/out/Coq__Arith__PeanoNat.dk.gz differ
diff --git a/out/Coq__Arith__Peano__dec.dk.gz b/out/Coq__Arith__Peano__dec.dk.gz
new file mode 100644
index 000000000..1581b50ef
Binary files /dev/null and b/out/Coq__Arith__Peano__dec.dk.gz differ
diff --git a/out/Coq__Arith__Plus.dk.gz b/out/Coq__Arith__Plus.dk.gz
new file mode 100644
index 000000000..417e7499a
Binary files /dev/null and b/out/Coq__Arith__Plus.dk.gz differ
diff --git a/out/Coq__Arith__Wf__nat.dk.gz b/out/Coq__Arith__Wf__nat.dk.gz
new file mode 100644
index 000000000..276a3fc72
Binary files /dev/null and b/out/Coq__Arith__Wf__nat.dk.gz differ
diff --git a/out/Coq__Bool__Bool.dk.gz b/out/Coq__Bool__Bool.dk.gz
new file mode 100644
index 000000000..f3df1dee8
Binary files /dev/null and b/out/Coq__Bool__Bool.dk.gz differ
diff --git a/out/Coq__Bool__BoolEq.dk.gz b/out/Coq__Bool__BoolEq.dk.gz
new file mode 100644
index 000000000..e284fa374
Binary files /dev/null and b/out/Coq__Bool__BoolEq.dk.gz differ
diff --git a/out/Coq__Bool__DecBool.dk.gz b/out/Coq__Bool__DecBool.dk.gz
new file mode 100644
index 000000000..375f5ac99
Binary files /dev/null and b/out/Coq__Bool__DecBool.dk.gz differ
diff --git a/out/Coq__Bool__IfProp.dk.gz b/out/Coq__Bool__IfProp.dk.gz
new file mode 100644
index 000000000..3b6050da5
Binary files /dev/null and b/out/Coq__Bool__IfProp.dk.gz differ
diff --git a/out/Coq__Classes__CMorphisms.dk.gz b/out/Coq__Classes__CMorphisms.dk.gz
new file mode 100644
index 000000000..25e1b781b
Binary files /dev/null and b/out/Coq__Classes__CMorphisms.dk.gz differ
diff --git a/out/Coq__Classes__CRelationClasses.dk.gz b/out/Coq__Classes__CRelationClasses.dk.gz
new file mode 100644
index 000000000..35f5411e9
Binary files /dev/null and b/out/Coq__Classes__CRelationClasses.dk.gz differ
diff --git a/out/Coq__Classes__Equivalence.dk.gz b/out/Coq__Classes__Equivalence.dk.gz
new file mode 100644
index 000000000..ede470903
Binary files /dev/null and b/out/Coq__Classes__Equivalence.dk.gz differ
diff --git a/out/Coq__Classes__Init.dk.gz b/out/Coq__Classes__Init.dk.gz
new file mode 100644
index 000000000..aacdf31e8
Binary files /dev/null and b/out/Coq__Classes__Init.dk.gz differ
diff --git a/out/Coq__Classes__Morphisms.dk.gz b/out/Coq__Classes__Morphisms.dk.gz
new file mode 100644
index 000000000..062e31994
Binary files /dev/null and b/out/Coq__Classes__Morphisms.dk.gz differ
diff --git a/out/Coq__Classes__Morphisms__Prop.dk.gz b/out/Coq__Classes__Morphisms__Prop.dk.gz
new file mode 100644
index 000000000..92502e27a
Binary files /dev/null and b/out/Coq__Classes__Morphisms__Prop.dk.gz differ
diff --git a/out/Coq__Classes__RelationClasses.dk.gz b/out/Coq__Classes__RelationClasses.dk.gz
new file mode 100644
index 000000000..28023a2ba
Binary files /dev/null and b/out/Coq__Classes__RelationClasses.dk.gz differ
diff --git a/out/Coq__Classes__SetoidTactics.dk.gz b/out/Coq__Classes__SetoidTactics.dk.gz
new file mode 100644
index 000000000..532e76416
Binary files /dev/null and b/out/Coq__Classes__SetoidTactics.dk.gz differ
diff --git a/out/Coq__Init__Datatypes.dk.gz b/out/Coq__Init__Datatypes.dk.gz
new file mode 100644
index 000000000..26afc7401
Binary files /dev/null and b/out/Coq__Init__Datatypes.dk.gz differ
diff --git a/out/Coq__Init__Decimal.dk.gz b/out/Coq__Init__Decimal.dk.gz
new file mode 100644
index 000000000..d462935ff
Binary files /dev/null and b/out/Coq__Init__Decimal.dk.gz differ
diff --git a/out/Coq__Init__Logic.dk.gz b/out/Coq__Init__Logic.dk.gz
new file mode 100644
index 000000000..eaa9766c0
Binary files /dev/null and b/out/Coq__Init__Logic.dk.gz differ
diff --git a/out/Coq__Init__Logic__Type.dk.gz b/out/Coq__Init__Logic__Type.dk.gz
new file mode 100644
index 000000000..a5d887ff9
Binary files /dev/null and b/out/Coq__Init__Logic__Type.dk.gz differ
diff --git a/out/Coq__Init__Nat.dk.gz b/out/Coq__Init__Nat.dk.gz
new file mode 100644
index 000000000..ce08318aa
Binary files /dev/null and b/out/Coq__Init__Nat.dk.gz differ
diff --git a/out/Coq__Init__Notations.dk.gz b/out/Coq__Init__Notations.dk.gz
new file mode 100644
index 000000000..c0f5860b2
Binary files /dev/null and b/out/Coq__Init__Notations.dk.gz differ
diff --git a/out/Coq__Init__Peano.dk.gz b/out/Coq__Init__Peano.dk.gz
new file mode 100644
index 000000000..976feba0b
Binary files /dev/null and b/out/Coq__Init__Peano.dk.gz differ
diff --git a/out/Coq__Init__Prelude.dk.gz b/out/Coq__Init__Prelude.dk.gz
new file mode 100644
index 000000000..8381b626a
Binary files /dev/null and b/out/Coq__Init__Prelude.dk.gz differ
diff --git a/out/Coq__Init__Specif.dk.gz b/out/Coq__Init__Specif.dk.gz
new file mode 100644
index 000000000..2ef9efde2
Binary files /dev/null and b/out/Coq__Init__Specif.dk.gz differ
diff --git a/out/Coq__Init__Tactics.dk.gz b/out/Coq__Init__Tactics.dk.gz
new file mode 100644
index 000000000..63b790254
Binary files /dev/null and b/out/Coq__Init__Tactics.dk.gz differ
diff --git a/out/Coq__Init__Tauto.dk.gz b/out/Coq__Init__Tauto.dk.gz
new file mode 100644
index 000000000..dbd967de0
Binary files /dev/null and b/out/Coq__Init__Tauto.dk.gz differ
diff --git a/out/Coq__Init__Wf.dk.gz b/out/Coq__Init__Wf.dk.gz
new file mode 100644
index 000000000..93c33c58a
Binary files /dev/null and b/out/Coq__Init__Wf.dk.gz differ
diff --git a/out/Coq__Logic__Decidable.dk.gz b/out/Coq__Logic__Decidable.dk.gz
new file mode 100644
index 000000000..4bab0f790
Binary files /dev/null and b/out/Coq__Logic__Decidable.dk.gz differ
diff --git a/out/Coq__Logic__EqdepFacts.dk.gz b/out/Coq__Logic__EqdepFacts.dk.gz
new file mode 100644
index 000000000..13e1f0c1c
Binary files /dev/null and b/out/Coq__Logic__EqdepFacts.dk.gz differ
diff --git a/out/Coq__Logic__Eqdep__dec.dk.gz b/out/Coq__Logic__Eqdep__dec.dk.gz
new file mode 100644
index 000000000..b7029868d
Binary files /dev/null and b/out/Coq__Logic__Eqdep__dec.dk.gz differ
diff --git a/out/Coq__Logic__ProofIrrelevanceFacts.dk.gz b/out/Coq__Logic__ProofIrrelevanceFacts.dk.gz
new file mode 100644
index 000000000..bf11c586f
Binary files /dev/null and b/out/Coq__Logic__ProofIrrelevanceFacts.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZAdd.dk.gz b/out/Coq__Numbers__NatInt__NZAdd.dk.gz
new file mode 100644
index 000000000..e100900a7
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZAdd.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZAddOrder.dk.gz b/out/Coq__Numbers__NatInt__NZAddOrder.dk.gz
new file mode 100644
index 000000000..98ba72fde
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZAddOrder.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZAxioms.dk.gz b/out/Coq__Numbers__NatInt__NZAxioms.dk.gz
new file mode 100644
index 000000000..a93382a27
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZAxioms.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZBase.dk.gz b/out/Coq__Numbers__NatInt__NZBase.dk.gz
new file mode 100644
index 000000000..b4d394c17
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZBase.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZBits.dk.gz b/out/Coq__Numbers__NatInt__NZBits.dk.gz
new file mode 100644
index 000000000..f5690e2e9
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZBits.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZDiv.dk.gz b/out/Coq__Numbers__NatInt__NZDiv.dk.gz
new file mode 100644
index 000000000..4bcc31a1a
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZDiv.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZGcd.dk.gz b/out/Coq__Numbers__NatInt__NZGcd.dk.gz
new file mode 100644
index 000000000..bb5a9d205
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZGcd.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZLog.dk.gz b/out/Coq__Numbers__NatInt__NZLog.dk.gz
new file mode 100644
index 000000000..38a934446
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZLog.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZMul.dk.gz b/out/Coq__Numbers__NatInt__NZMul.dk.gz
new file mode 100644
index 000000000..93b627f53
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZMul.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZMulOrder.dk.gz b/out/Coq__Numbers__NatInt__NZMulOrder.dk.gz
new file mode 100644
index 000000000..d1c31101e
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZMulOrder.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZOrder.dk.gz b/out/Coq__Numbers__NatInt__NZOrder.dk.gz
new file mode 100644
index 000000000..145ca7c1b
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZOrder.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZParity.dk.gz b/out/Coq__Numbers__NatInt__NZParity.dk.gz
new file mode 100644
index 000000000..6cc7c93e9
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZParity.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZPow.dk.gz b/out/Coq__Numbers__NatInt__NZPow.dk.gz
new file mode 100644
index 000000000..256eb3d39
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZPow.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZProperties.dk.gz b/out/Coq__Numbers__NatInt__NZProperties.dk.gz
new file mode 100644
index 000000000..2c49f5a2f
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZProperties.dk.gz differ
diff --git a/out/Coq__Numbers__NatInt__NZSqrt.dk.gz b/out/Coq__Numbers__NatInt__NZSqrt.dk.gz
new file mode 100644
index 000000000..299cde8f7
Binary files /dev/null and b/out/Coq__Numbers__NatInt__NZSqrt.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NAdd.dk.gz b/out/Coq__Numbers__Natural__Abstract__NAdd.dk.gz
new file mode 100644
index 000000000..daf4f364e
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NAdd.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NAddOrder.dk.gz b/out/Coq__Numbers__Natural__Abstract__NAddOrder.dk.gz
new file mode 100644
index 000000000..2a6c9b088
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NAddOrder.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NAxioms.dk.gz b/out/Coq__Numbers__Natural__Abstract__NAxioms.dk.gz
new file mode 100644
index 000000000..74b39cb93
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NAxioms.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NBase.dk.gz b/out/Coq__Numbers__Natural__Abstract__NBase.dk.gz
new file mode 100644
index 000000000..b6825e577
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NBase.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NBits.dk.gz b/out/Coq__Numbers__Natural__Abstract__NBits.dk.gz
new file mode 100644
index 000000000..6379013b1
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NBits.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NDiv.dk.gz b/out/Coq__Numbers__Natural__Abstract__NDiv.dk.gz
new file mode 100644
index 000000000..7e8477904
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NDiv.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NGcd.dk.gz b/out/Coq__Numbers__Natural__Abstract__NGcd.dk.gz
new file mode 100644
index 000000000..8f2f0b8d0
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NGcd.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NLcm.dk.gz b/out/Coq__Numbers__Natural__Abstract__NLcm.dk.gz
new file mode 100644
index 000000000..1b917f312
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NLcm.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NLog.dk.gz b/out/Coq__Numbers__Natural__Abstract__NLog.dk.gz
new file mode 100644
index 000000000..ffefa732e
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NLog.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NMaxMin.dk.gz b/out/Coq__Numbers__Natural__Abstract__NMaxMin.dk.gz
new file mode 100644
index 000000000..981b66748
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NMaxMin.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NMulOrder.dk.gz b/out/Coq__Numbers__Natural__Abstract__NMulOrder.dk.gz
new file mode 100644
index 000000000..598c57a15
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NMulOrder.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NOrder.dk.gz b/out/Coq__Numbers__Natural__Abstract__NOrder.dk.gz
new file mode 100644
index 000000000..723c1fd01
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NOrder.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NParity.dk.gz b/out/Coq__Numbers__Natural__Abstract__NParity.dk.gz
new file mode 100644
index 000000000..238775f55
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NParity.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NPow.dk.gz b/out/Coq__Numbers__Natural__Abstract__NPow.dk.gz
new file mode 100644
index 000000000..27c6e88d9
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NPow.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NProperties.dk.gz b/out/Coq__Numbers__Natural__Abstract__NProperties.dk.gz
new file mode 100644
index 000000000..1c8d45f05
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NProperties.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NSqrt.dk.gz b/out/Coq__Numbers__Natural__Abstract__NSqrt.dk.gz
new file mode 100644
index 000000000..ef0c77360
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NSqrt.dk.gz differ
diff --git a/out/Coq__Numbers__Natural__Abstract__NSub.dk.gz b/out/Coq__Numbers__Natural__Abstract__NSub.dk.gz
new file mode 100644
index 000000000..e9711ca8a
Binary files /dev/null and b/out/Coq__Numbers__Natural__Abstract__NSub.dk.gz differ
diff --git a/out/Coq__Numbers__NumPrelude.dk.gz b/out/Coq__Numbers__NumPrelude.dk.gz
new file mode 100644
index 000000000..56970db5c
Binary files /dev/null and b/out/Coq__Numbers__NumPrelude.dk.gz differ
diff --git a/out/Coq__Program__Basics.dk.gz b/out/Coq__Program__Basics.dk.gz
new file mode 100644
index 000000000..2d7d0145b
Binary files /dev/null and b/out/Coq__Program__Basics.dk.gz differ
diff --git a/out/Coq__Program__Tactics.dk.gz b/out/Coq__Program__Tactics.dk.gz
new file mode 100644
index 000000000..936eecb11
Binary files /dev/null and b/out/Coq__Program__Tactics.dk.gz differ
diff --git a/out/Coq__Relations__Operators__Properties.dk.gz b/out/Coq__Relations__Operators__Properties.dk.gz
new file mode 100644
index 000000000..748b18310
Binary files /dev/null and b/out/Coq__Relations__Operators__Properties.dk.gz differ
diff --git a/out/Coq__Relations__Relation__Definitions.dk.gz b/out/Coq__Relations__Relation__Definitions.dk.gz
new file mode 100644
index 000000000..2aa946ddb
Binary files /dev/null and b/out/Coq__Relations__Relation__Definitions.dk.gz differ
diff --git a/out/Coq__Relations__Relation__Operators.dk.gz b/out/Coq__Relations__Relation__Operators.dk.gz
new file mode 100644
index 000000000..c77ab7838
Binary files /dev/null and b/out/Coq__Relations__Relation__Operators.dk.gz differ
diff --git a/out/Coq__Relations__Relations.dk.gz b/out/Coq__Relations__Relations.dk.gz
new file mode 100644
index 000000000..60b9e63b0
Binary files /dev/null and b/out/Coq__Relations__Relations.dk.gz differ
diff --git a/out/Coq__Setoids__Setoid.dk.gz b/out/Coq__Setoids__Setoid.dk.gz
new file mode 100644
index 000000000..07c3ab239
Binary files /dev/null and b/out/Coq__Setoids__Setoid.dk.gz differ
diff --git a/out/Coq__Structures__Equalities.dk.gz b/out/Coq__Structures__Equalities.dk.gz
new file mode 100644
index 000000000..e44a9e182
Binary files /dev/null and b/out/Coq__Structures__Equalities.dk.gz differ
diff --git a/out/Coq__Structures__GenericMinMax.dk.gz b/out/Coq__Structures__GenericMinMax.dk.gz
new file mode 100644
index 000000000..b7082b753
Binary files /dev/null and b/out/Coq__Structures__GenericMinMax.dk.gz differ
diff --git a/out/Coq__Structures__Orders.dk.gz b/out/Coq__Structures__Orders.dk.gz
new file mode 100644
index 000000000..47659c862
Binary files /dev/null and b/out/Coq__Structures__Orders.dk.gz differ
diff --git a/out/Coq__Structures__OrdersFacts.dk.gz b/out/Coq__Structures__OrdersFacts.dk.gz
new file mode 100644
index 000000000..865261eb7
Binary files /dev/null and b/out/Coq__Structures__OrdersFacts.dk.gz differ
diff --git a/out/Coq__Structures__OrdersTac.dk.gz b/out/Coq__Structures__OrdersTac.dk.gz
new file mode 100644
index 000000000..90fa4362b
Binary files /dev/null and b/out/Coq__Structures__OrdersTac.dk.gz differ
diff --git a/out/add_requires.sh b/out/add_requires.sh
new file mode 100755
index 000000000..bdabc750e
--- /dev/null
+++ b/out/add_requires.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+dk dep $@ | cut -d ":" -f 2 | sed "s/ /\n/g" | grep ".dko$" | sed "s/\(.*\)\.dko$/require coq.\\1 as \\1;/g"
diff --git a/out/compile.sh b/out/compile.sh
new file mode 100755
index 000000000..f8fff5b90
--- /dev/null
+++ b/out/compile.sh
@@ -0,0 +1,22 @@
+#!/bin/sh
+#set -e
+#set -x
+
+#export PATH=$PWD/_build/install/default/bin:$PATH
+
+for i in *.dk.gz; do rm -f `basename $i .gz`; gunzip -k $i; done
+touch cupicef.dk
+
+for i in *.dk; do
+  LPFILE=`basename $i .dk`.lp
+  # add the flags
+  cat header > $LPFILE
+  # add the exports
+  ./add_requires.sh $i >> $LPFILE
+  lambdapi export -o lp $i >> $LPFILE ;
+done
+cp cupicef.lp.handmade cupicef.lp
+
+rm *.dk
+
+lambdapi check -c Coq__Init__Peano.lp
diff --git a/out/cupicef.lp.handmade b/out/cupicef.lp.handmade
new file mode 100644
index 000000000..9a4f1fa1f
--- /dev/null
+++ b/out/cupicef.lp.handmade
@@ -0,0 +1,373 @@
+constant symbol Sort : TYPE;
+symbol sup : Sort → Sort → Sort;
+constant symbol Univ : Π (s : Sort), TYPE;
+symbol Term : Π (s : Sort), Π (a : Univ s), TYPE;
+constant symbol Bool : TYPE;
+constant symbol eps : Bool → TYPE;
+constant symbol true : Bool;
+constant symbol I : eps true;
+symbol Axiom : Sort → Sort → Bool;
+symbol Rule : Sort → Sort → Sort → Bool;
+symbol Cumul : Sort → Sort → Bool;
+symbol Eq : Sort → Sort → Bool;
+rule Eq $x $x ↪ true;
+associative commutative symbol and : Bool → Bool → Bool;
+associative commutative symbol or : Bool → Bool → Bool;
+rule and true $c ↪ $c;
+rule and $c true ↪ $c;
+rule or true $c ↪ true;
+rule or $c true ↪ true;
+symbol BoolO : TYPE;
+constant symbol BoolNone : BoolO;
+constant symbol BoolSome : Bool → BoolO;
+symbol Multi : Bool → BoolO → TYPE;
+rule Multi $A BoolNone ↪ eps $A
+with Multi $A (BoolSome $B) ↪ eps $B
+                                → Π (C : BoolO), Multi (and $A $B) C;
+constant symbol pair : Π (A : BoolO), Multi true A;
+symbol SortO : TYPE;
+constant symbol SortNone : SortO;
+constant symbol SortSome : Sort → SortO;
+symbol Trans : Sort → Sort → SortO → TYPE;
+rule Trans $s1 $s2 SortNone ↪ eps (Cumul $s1 $s2)
+with Trans $s1 $s2 (SortSome $s3) ↪ eps (Cumul $s2 $s3)
+                                      → Π (so : SortO), Trans $s1 $s3 so;
+constant symbol trans : Π (s : Sort), Π (so : SortO), Trans s s so;
+constant symbol cumul_eq
+  : Π (s1 : Sort), Π (s2 : Sort), eps (Eq s1 s2) → eps (Cumul s1 s2);
+constant symbol eq_sym
+  : Π (s1 : Sort), Π (s2 : Sort), eps (Eq s1 s2) → eps (Eq s2 s1);
+symbol univ : Π (s : Sort), Π (s' : Sort), eps (Axiom s s') → Univ s';
+symbol prod
+  : Π (s1 : Sort),
+      Π (s2 : Sort),
+        Π (s3 : Sort),
+          eps (Rule s1 s2 s3)
+          → Π (a : Univ s1), Π (b : Term s1 a → Univ s2), Univ s3;
+symbol SubType : Π (s : Sort), Π (s' : Sort), Univ s → Univ s' → Bool;
+symbol cast
+  : Π (s : Sort),
+      Π (s' : Sort),
+        Π (a : Univ s),
+          Π (b : Univ s'), eps (SubType s s' a b) → Term s a → Term s' b;
+constant symbol sinf : Sort;
+symbol Code ≔ Univ sinf;
+//injective symbol Decode : Code → TYPE;
+symbol Decode : Code → TYPE;
+//injective symbol uncode : Π (t : Code), Code → Decode t;
+symbol uncode : Π (t : Code), Code → Decode t;
+//injective symbol code : Π (t : Code), Decode t → Code;
+symbol code : Π (t : Code), Decode t → Code;
+constant symbol cU : Π (s : Sort), Code;
+constant symbol cPi : Π (A : Code), (Decode A → Code) → Code;
+constant symbol cLam : Π (A : Code), (Decode A → Code) → Code;
+symbol cApp : Code → Code → Code;
+rule Decode (cU $s) ↪ Univ $s;
+rule Decode (cPi $a $b) ↪ Π (x : Decode $a), Decode ($b x);
+rule code (cU sinf) $t ↪ $t;
+rule uncode (cU sinf) $t ↪ $t;
+rule Term $s $t ↪ Decode (code (cU $s) $t);
+rule univ $s $s' $p ↪ uncode (cU $s') (cU $s);
+rule prod $s1 $s2 $s3 $p $a $b ↪ uncode (cU $s3)
+                                   (cPi (code (cU $s1) $a)
+                                    (λ x, code (cU $s2.[]) ($b.[] x)));
+rule cast $s1 $s2 $a $b _ $t ↪ uncode (code (cU $s2) $b)
+                                 (code (code (cU $s1) $a) $t);
+rule Cumul $s $s ↪ true;
+symbol forall : (Code → Bool) → Bool;
+rule forall (λ x, $B.[]) ↪ $B;
+symbol ST : Code → Code → Bool;
+symbol EQ : Code → Code → Bool;
+rule ST (cU $s1) (cU $s2) ↪ Cumul $s1 $s2;
+rule EQ (cU $s1) (cU $s2) ↪ Eq $s1 $s2;
+rule ST (cPi $a $b) (cPi $a' $b') ↪ and (EQ $a $a')
+                                      (forall
+                                       (λ (x : Code),
+                                          ST ($b.[] (uncode $a.[] x))
+                                          ($b'.[] (uncode $a'.[] x))));
+rule EQ (cPi $a $b) (cPi $a' $b') ↪ and (EQ $a $a')
+                                      (forall
+                                       (λ (x : Code),
+                                          EQ ($b.[] (uncode $a.[] x))
+                                          ($b'.[] (uncode $a'.[] x))));
+rule EQ $A $A ↪ true;
+rule ST $A $A ↪ true;
+rule SubType $sa $sb $a $b ↪ ST (code (cU $sa) $a) (code (cU $sb) $b);
+rule code _ (uncode _ $t) ↪ $t;
+rule code (cPi $A $B) $F ↪ cLam $A
+                             (λ (x : Decode $A), code ($B.[] x) ($F.[] x));
+rule uncode (cPi $A $B) $F $U ↪ uncode ($B $U) (cApp $F (code $A $U));
+rule uncode (cPi $A $B) (cLam $A' $F) ↪ λ (x : Decode $A),
+                                            uncode ($B x)
+                                            ($F (uncode $A' (code $A x)));
+rule cApp (code (cPi $A $B) $F) $U ↪ code ($B (uncode $A $U))
+                                       ($F (uncode $A $U));
+rule cApp (cLam $A $F) $U ↪ $F (uncode $A $U);
+rule uncode $s (code $s $t) ↪ $t;
+symbol univ' (s : Sort) (s' : Sort) ≔ uncode (cU s') (cU s);
+symbol lift' (s : Sort) (s' : Sort) (t : Univ s)
+  ≔ uncode (cU s') (code (cU s) t);
+symbol prod' (s1 : Sort) (s2 : Sort) (s : Sort) (A : Univ s1)
+  (B : Term s1 A → Univ s2) : Univ s
+  ≔ uncode (cU s) (cPi (code (cU s1) A) (λ x, code (cU s2) (B x)));
+constant symbol Nat : TYPE;
+symbol s : Nat → Nat;
+constant symbol z : Nat;
+constant symbol prop : Sort;
+constant symbol {|type|} : Nat → Sort;
+symbol set : Sort ≔ {|type|} z;
+symbol type0 : Sort ≔ {|type|} (s z);
+associative commutative symbol max : Nat → Nat → Nat;
+rule max $i z ↪ $i;
+rule s (max $i $j) ↪ max (s $i) (s $j);
+rule max $i $i ↪ $i
+with max $i (max $i $j) ↪ max $i $j
+with max $i (s $i) ↪ s $i
+with max $i (max (s $i) $j) ↪ max (s $i) $j
+with max $i (s (max $i $j)) ↪ s (max $i $j)
+with max (max $i $k) (s (max $i $j)) ↪ max $k (s (max $i $j));
+
+rule max z $i ↪ $i;
+rule max (max $i $j) $i ↪ max $i $j
+with max (max $j $i) $i ↪ max $i $j
+with max $i (max $j $i) ↪ max $i $j
+with max (s $i) $i ↪ s $i
+with max (max (s $i) $j) $i ↪ max (s $i) $j
+with max (max $j (s $i)) $i ↪ max (s $i) $j
+with max $i (max $j (s $i)) ↪ max (s $i) $j
+with max $i (s (max $j $i)) ↪ s (max $i $j)
+with max (s (max $i $j)) $i ↪ s (max $i $j)
+with max (s (max $j $i)) $i ↪ s (max $i $j)
+with max (max $k $i) (s (max $i $j)) ↪ max $k (s (max $i $j))
+with max (max $k $i) (s (max $j $i)) ↪ max $k (s (max $i $j))
+with max (max $i $k) (s (max $j $i)) ↪ max $k (s (max $i $j))
+with max (s (max $i $j)) (max $i $k) ↪ max $k (s (max $i $j))
+with max (s (max $i $j)) (max $k $i) ↪ max $k (s (max $i $j))
+with max (s (max $j $i)) (max $i $k) ↪ max $k (s (max $i $j))
+with max (s (max $j $i)) (max $k $i) ↪ max $k (s (max $i $j));
+
+rule sup prop $s ↪ $s
+with sup $s prop ↪ $s
+with sup ({|type|} $i) ({|type|} $j) ↪ {|type|} (max $i $j);
+sequential symbol Leq : Nat → Nat → Bool;
+rule Leq z $j ↪ true
+with Leq (s $i) (s $j) ↪ Leq $i $j
+with Leq (max $i $j) $k ↪ and (Leq $i $k) (Leq $j $k)
+with Leq $i $i ↪ true
+with Leq $i (s $i) ↪ true
+with Leq $i (max $i $j) ↪ true
+with Leq $i (max $j $i) ↪ true
+with Leq $i (max (s $i) $j) ↪ true
+with Leq $i (max $j (s $i)) ↪ true;
+
+rule Leq $i (max $j $k) ↪ or (Leq $i $j) (Leq $i $k);
+
+rule Axiom prop ({|type|} _) ↪ true
+with Axiom ({|type|} $i) ({|type|} $j) ↪ Leq $i $j;
+rule Rule _ prop prop ↪ true
+with Rule prop ({|type|} $i) ({|type|} $i) ↪ true
+with Rule ({|type|} $i) ({|type|} $j) ({|type|} $k) ↪ Leq (max $i $j) $k;
+rule Cumul prop prop ↪ true
+with Cumul prop ({|type|} $i) ↪ true
+with Cumul ({|type|} $i) ({|type|} $j) ↪ Leq $i $j;
+symbol axiom : Sort → Sort;
+rule axiom prop ↪ {|type|} z
+with axiom ({|type|} $i) ↪ {|type|} (s $i);
+rule Axiom $x (axiom $x) ↪ true;
+symbol {|rule|} : Sort → Sort → Sort;
+rule {|rule|} prop $s ↪ $s
+with {|rule|} _ prop ↪ prop
+with {|rule|} ({|type|} $i) ({|type|} $j) ↪ {|type|} (max $i $j);
+rule Rule $s1 $s2 ({|rule|} $s1 $s2) ↪ true;
+rule Rule $s $s $s ↪ true;
+constant symbol N : TYPE;
+constant symbol 0 : N;
+constant symbol _S : N → N;
+symbol 1 ≔ _S 0;
+symbol 2 ≔ _S 1;
+symbol 3 ≔ _S 2;
+symbol 4 ≔ _S 3;
+symbol 5 ≔ _S 4;
+symbol 6 ≔ _S 5;
+symbol 7 ≔ _S 6;
+symbol 8 ≔ _S 7;
+symbol 9 ≔ _S 8;
+constant symbol SingleArity : TYPE;
+constant symbol SAcons : N → Code → SingleArity;
+symbol SA_code : SingleArity → Code;
+rule SA_code (SAcons _ $A) ↪ $A;
+constant symbol MutualArity : N → TYPE;
+constant symbol MAnil : MutualArity 0;
+constant symbol MAcons
+  : Π (n : N), SingleArity → MutualArity n → MutualArity (_S n);
+symbol MA_ith_SA : Π (n : N), MutualArity n → N → SingleArity;
+rule MA_ith_SA _ (MAcons _ $SA _) 0 ↪ $SA;
+rule MA_ith_SA _ (MAcons $n _ $MA) (_S $i) ↪ MA_ith_SA $n $MA $i;
+symbol MA_ith_code (n : N) (MA : MutualArity n) (i : N) : Code
+  ≔ SA_code (MA_ith_SA n MA i);
+symbol MA_lift_code : Code → Π (m : N), MutualArity m → Code;
+rule MA_lift_code $B _ MAnil ↪ $B;
+rule MA_lift_code $B _ (MAcons $m $SA $MA) ↪ cPi (SA_code $SA)
+                                               (λ f,
+                                                  MA_lift_code $B.[] $m.[]
+                                                  $MA.[]);
+symbol MA_code (n : N) (MA : MutualArity n) (i : N) : Code
+  ≔ MA_lift_code (MA_ith_code n MA i) n MA;
+constant symbol MutualFixpointAux
+  : Π (n : N), MutualArity n → Π (i : N), MutualArity i → TYPE;
+symbol MutualFixpoint (n : N) (MA : MutualArity n) : TYPE
+  ≔ MutualFixpointAux n MA n MA;
+constant symbol MFTnil
+  : Π (n : N), Π (MA : MutualArity n), MutualFixpointAux n MA 0 MAnil;
+constant symbol MFTcons
+  : Π (n : N),
+      Π (MAn : MutualArity n),
+        Π (i : N),
+          Π (MAi : MutualArity i),
+            Π (SA : SingleArity),
+              Decode (MA_lift_code (SA_code SA) n MAn)
+              → MutualFixpointAux n MAn i MAi
+                  → MutualFixpointAux n MAn (_S i) (MAcons i SA MAi);
+symbol fix_body
+  : Π (n : N),
+      Π (MA : MutualArity n),
+        MutualFixpoint n MA → Π (i : N), Decode (MA_code n MA i);
+symbol fix_body'
+  : Π (n : N),
+      Π (MAn : MutualArity n),
+        Π (i : N),
+          Π (MAi : MutualArity i),
+            MutualFixpointAux n MAn i MAi
+            → Π (j : N),
+                  Decode (MA_lift_code (SA_code (MA_ith_SA i MAi j)) n MAn);
+rule fix_body $n $MA $MF $i ↪ fix_body' $n $MA $n $MA $MF $i;
+rule fix_body' $n $MA (_S _) (MAcons _ $SA _) (MFTcons _ _ _ _ _ $t _) 0 ↪ $t;
+rule fix_body' $n $MA (_S _) (MAcons $i _ $MAi) (MFTcons _ _ _ _ _ _ $MFT)
+     (_S $j) ↪ fix_body' $n $MA $i $MAi $MFT $j;
+symbol app_body
+  : Π (n : N),
+      Π (MA : MutualArity n),
+        Π (A : Code),
+          Π (B : Decode A → Code),
+            Π (body : Decode (MA_lift_code (cPi A B) n MA)),
+              Π (a : Decode A), Decode (MA_lift_code (B a) n MA);
+rule app_body _ MAnil _ _ $body $a ↪ $body $a;
+rule app_body _ (MAcons $n $SA $MA) $A $B $body $a ↪ λ
+                                                         (
+                                                         f : Decode
+                                                             (SA_code $SA)
+                                                         ),
+                                                         app_body $n $MA $A
+                                                         $B ($body f) $a;
+constant symbol Guarded? : TYPE;
+constant symbol guarded : Guarded?;
+symbol code_guarded? : Π (Ind : Code), Decode Ind → Guarded?;
+symbol guarded? : Π (s : Sort), Π (Ind : Univ s), Term s Ind → Guarded?;
+rule guarded? $s $Ind $c ↪ code_guarded? (code (cU $s) $Ind) $c;
+symbol fix_proj
+  : Π (n : N),
+      Π (MA : MutualArity n),
+        MutualFixpoint n MA → Π (i : N), Decode (MA_ith_code n MA i);
+symbol fix_proj_1
+  : Π (n : N),
+      Π (MA : MutualArity n),
+        MutualFixpoint n MA
+        → Π (SA : SingleArity),
+              Decode (MA_lift_code (SA_code SA) n MA) → Decode (SA_code SA);
+rule fix_proj $n $MA $MF $i ↪ fix_proj_1 $n $MA $MF (MA_ith_SA $n $MA $i)
+                                (fix_body $n $MA $MF $i);
+rule fix_proj_1 $n $MA $MF (SAcons (_S $i) (cPi $A $B)) $body $a ↪ 
+fix_proj_1 $n $MA $MF (SAcons $i ($B $a)) (app_body $n $MA $A $B $body $a);
+symbol fix_proj_2
+  : Π (n : N),
+      Π (MA : MutualArity n),
+        MutualFixpoint n MA
+        → Π (A : Code),
+              Decode (MA_lift_code A n MA) → Guarded? → Decode A;
+rule fix_proj_1 $n $MA $MF (SAcons 0 (cPi $Ind $B)) $body $a ↪ fix_proj_2
+                                                                 $n $MA $MF
+                                                                 (cPi $Ind $B)
+                                                                 $body
+                                                                 (code_guarded?
+                                                                  $Ind $a)
+                                                                 $a;
+symbol fix_proj_3
+  : Π (A : Code),
+      Π (i : N),
+        Π (MAi : MutualArity i),
+          Π (f : Π (k : N), Decode (MA_ith_code i MAi k)),
+            Decode (MA_lift_code A i MAi) → Decode A;
+rule fix_proj_2 $n $MA $MF $A $body guarded ↪ fix_proj_3 $A $n $MA
+                                                (λ (k : N),
+                                                   fix_proj $n.[] $MA.[]
+                                                   $MF.[] k)
+                                                $body;
+rule fix_proj_3 _ _ MAnil _ $body ↪ $body;
+rule fix_proj_3 $A _ (MAcons $i _ $MAi) $f $body ↪ fix_proj_3 $A $i $MAi
+                                                     (λ (k : N),
+                                                        $f.[] (_S k))
+                                                     ($body ($f 0));
+symbol MutualArity' : N → N → TYPE;
+rule MutualArity' $n 0 ↪ MutualArity $n;
+rule MutualArity' $n (_S $i) ↪ SingleArity → MutualArity' $n $i;
+symbol MA_magic
+  : Π (n : N),
+      Π (m : N), SingleArity → MutualArity' n m → MutualArity' (_S n) m;
+rule MA_magic $n 0 $A $MA ↪ MAcons $n $A $MA;
+rule MA_magic $n (_S $m) $A $MA $A' ↪ MA_magic $n $m $A ($MA $A');
+symbol make_MA : Π (n : N), MutualArity' n n;
+rule make_MA 0 ↪ MAnil;
+rule make_MA (_S $n) $SA ↪ MA_magic $n $n $SA (make_MA $n);
+symbol MutualFixpoint'
+  : Π (n : N),
+      MutualArity n
+      → Π (i : N), MutualArity i → Π (j : N), MutualArity j → TYPE;
+rule MutualFixpoint' $n $MAn $i $MAi _ MAnil ↪ MutualFixpointAux $n $MAn $i
+                                                 $MAi;
+rule MutualFixpoint' $n $MAn $i $MAi _ (MAcons $j $SA $MAj) ↪ Decode
+                                                                (MA_lift_code
+                                                                 (SA_code $SA)
+                                                                 $n $MAn)
+                                                                → MutualFixpoint'
+                                                                    $n $MAn
+                                                                    $i $MAi
+                                                                    $j $MAj;
+symbol fix_magic
+  : Π (n : N),
+      Π (MAn : MutualArity n),
+        Π (i : N),
+          Π (MAi : MutualArity i),
+            Π (j : N),
+              Π (MAj : MutualArity j),
+                Π (SA : SingleArity),
+                  Decode (MA_lift_code (SA_code SA) n MAn)
+                  → MutualFixpoint' n MAn i MAi j MAj
+                      → MutualFixpoint' n MAn (_S i) (MAcons i SA MAi) j
+                          MAj;
+rule fix_magic $n $MAn $i $MAi _ MAnil $SA $t $MFT ↪ MFTcons $n $MAn $i
+                                                       $MAi $SA $t $MFT;
+rule fix_magic $n $MAn $i $MAi (_S _) (MAcons $j _ $MAj) $SA $t $MFT $t' ↪ 
+fix_magic $n $MAn $i $MAi $j $MAj $SA $t ($MFT $t');
+symbol make_fix
+  : Π (n : N),
+      Π (MAn : MutualArity n),
+        Π (i : N),
+          Π (MAi : MutualArity i), MutualFixpoint' n MAn i MAi i MAi;
+rule make_fix $n $MAn _ MAnil ↪ MFTnil $n $MAn;
+rule make_fix $n $MAn (_S _) (MAcons $j $SA $MAj) $t ↪ fix_magic $n $MAn $j
+                                                         $MAj $j $MAj $SA $t
+                                                         (make_fix $n $MAn $j
+                                                          $MAj);
+symbol SA : N → Π (s : Sort), Univ s → SingleArity;
+rule SA $n $s $t ↪ SAcons $n (code (cU $s) $t);
+symbol fix
+  : Π (n : N), Π (MA : MutualArity n), MutualFixpoint' n MA n MA n MA;
+rule fix $n $MAn ↪ make_fix $n $MAn $n $MAn;
+symbol fixproj
+  : Π (n : N),
+      Π (MA : MutualArity' n n → MutualArity n),
+        (MutualFixpoint' n (MA (make_MA n)) n (MA (make_MA n)) n
+         (MA (make_MA n)) → MutualFixpoint n (MA (make_MA n)))
+        → Π (i : N), Decode (MA_ith_code n (MA (make_MA n)) i);
+rule fixproj $n $MA $MF ↪ fix_proj $n ($MA (make_MA $n))
+                            ($MF (fix $n ($MA (make_MA $n))));
diff --git a/out/header b/out/header
new file mode 100644
index 000000000..d390112cb
--- /dev/null
+++ b/out/header
@@ -0,0 +1 @@
+flag "eta_equality" on;
diff --git a/out/lambdapi.pkg b/out/lambdapi.pkg
new file mode 100644
index 000000000..798df43c1
--- /dev/null
+++ b/out/lambdapi.pkg
@@ -0,0 +1,2 @@
+package_name=coq
+root_path=coq
diff --git a/out/test.lp b/out/test.lp
new file mode 100644
index 000000000..eeb40923d
--- /dev/null
+++ b/out/test.lp
@@ -0,0 +1,53 @@
+require coq.cupicef as bios;
+require coq.Coq__Relations__Relation__Definitions;
+require coq.Coq__Classes__RelationClasses as x;
+require coq.Coq__Init__Logic as y;
+
+open "tc" coq.Coq__Classes__RelationClasses;
+
+flag "print_implicits" on; // default is off
+flag "print_contexts" on; // default is off
+flag "print_domains" on; // default is off
+flag "print_meta_types" on; // default is 
+
+type y.eq;
+type x.reflexivity;
+
+// ENRICO: bug in readback of terms in the query,the context is empty 
+// We hack it with a section variable
+symbol A : bios.Univ (bios.type (bios.s bios.z));
+
+// cast from Type[1] to Type[2]
+coerce_rule coerce (bios.Univ (bios.{|type|} (bios.s bios.z))) (bios.Univ (bios.{|type|} (bios.s (bios.s bios.z)))) $X ↪ (bios.cast (bios.axiom (bios.{|type|} (bios.s bios.z)))
+ (bios.axiom (bios.{|type|} (bios.s (bios.s bios.z))))
+ (bios.univ (bios.{|type|} (bios.s bios.z))
+  (bios.axiom (bios.{|type|} (bios.s bios.z))) bios.I)
+ (bios.univ (bios.{|type|} (bios.s (bios.s bios.z)))
+  (bios.axiom (bios.{|type|} (bios.s (bios.s bios.z)))) bios.I)
+ bios.I
+ $X);
+
+//debug +i;
+//debug +e;
+//debug +u;
+
+type x.reflexivity A (y.eq A) _ _;
+type x.match____RewriteRelation _ A (y.eq A) _ _ _;
+
+/*
+type
+x.reflexivity A (y.eq
+(
+    
+bios.cast
+(bios.axiom (bios.{|type|} (bios.s bios.z)))
+(bios.axiom (bios.{|type|} (bios.s (bios.s bios.z))))
+(bios.univ (bios.{|type|} (bios.s bios.z))
+ (bios.axiom (bios.{|type|} (bios.s bios.z))) bios.I)
+(bios.univ (bios.{|type|} (bios.s (bios.s bios.z)))
+ (bios.axiom (bios.{|type|} (bios.s (bios.s bios.z))))
+ bios.I)
+_
+
+A)) _ _;
+*/
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 0b05e9fcb..2338b1501 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -23,6 +23,7 @@ let check_cmd : Config.t -> int option -> string list -> unit =
   let run _ =
     let open Timed in
     Config.init cfg;
+    Elpi_handle.init ();
     (* We save time to run each file in the same environment. *)
     let time = Time.save () in
     let handle file =
diff --git a/src/common/error.ml b/src/common/error.ml
index 975284cc7..4eebc33d2 100644
--- a/src/common/error.ml
+++ b/src/common/error.ml
@@ -73,4 +73,6 @@ let handle_exceptions : (unit -> unit) -> unit = fun f ->
   try f () with
   | Fatal(None,    msg) -> exit_with "%s" msg
   | Fatal(Some(p), msg) -> exit_with "[%a] %s" Pos.pp p msg
+  (*
   | e                   -> exit_with "Uncaught [%s]." (Printexc.to_string e)
+  *)
diff --git a/src/core/ctxt.ml b/src/core/ctxt.ml
index e21d620ce..e8399426e 100644
--- a/src/core/ctxt.ml
+++ b/src/core/ctxt.ml
@@ -4,10 +4,22 @@ open Term
 open Lplib
 open Timed
 
+(** [unbind ctx a def b] returns a triple [(x,t,new_ctx)] such that [(x,t)] is
+    an unbinding of [b] (in the sense of [Bindlib.unbind]) and [new_ctx] is an
+    extension of context [ctx] with the assumption that [x] has type [a] (only
+    if [x] occurs in [t], or [~keep:true]).
+    If [def] is of the form [Some(u)], the context also
+    registers the term [u] as the definition of variable [x]. *)
+let unbind : ?keep:bool -> 'a actxt -> 'a -> term option -> tbinder ->
+  tvar * term * 'a actxt =
+  fun ?(keep=false) ctx a def b ->
+  let (x, t) = Bindlib.unbind b in
+  (x, t, if keep || Bindlib.binder_occur b then (x, a, def) :: ctx else ctx)
+
 (** [type_of x ctx] returns the type of [x] in the context [ctx] when it
     appears in it, and
 @raise [Not_found] otherwise. *)
-let type_of : tvar -> ctxt -> term = fun x ctx ->
+let type_of : tvar -> 'a actxt -> 'a = fun x ctx ->
   let (_,a,_) = List.find (fun (y,_,_) -> Bindlib.eq_vars x y) ctx in a
 
 (** [def_of x ctx] returns the definition of [x] in the context [ctx] if it
diff --git a/src/core/dune b/src/core/dune
index d0f25c063..4bbaa79de 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -10,4 +10,4 @@
  (public_name lambdapi.core)
  (synopsis "LambdaPi interactive theorem prover [core]")
  (modules :standard)
- (libraries lambdapi.common lambdapi.lplib pratter bindlib why3))
+ (libraries lambdapi.common lambdapi.lplib pratter bindlib why3 elpi))
diff --git a/src/core/elpi_lambdapi.ml b/src/core/elpi_lambdapi.ml
new file mode 100644
index 000000000..195f6f2cd
--- /dev/null
+++ b/src/core/elpi_lambdapi.ml
@@ -0,0 +1,262 @@
+open Elpi.API
+
+module Elpi_AUX = struct
+  let array_map_fold f st a =
+    let len = Array.length a in
+    let st = ref st in
+    let b = Array.make len RawData.mkNil in
+    for i = 0 to len-1 do
+      let st', x = f !st a.(i) in
+      st := st';
+      b.(i) <- x
+    done;
+    !st, b
+
+  let list_map_fold f s l =
+    let f st x = let st, x = f st x in st, x, [] in
+    let s, l, _ = Utils.map_acc f s l in
+    s, l
+
+  let loc_of_pos = function
+    | None -> Ast.Loc.initial "(elpi)"
+    | Some x ->
+        let { Common.Pos.fname; start_line; start_col; _ } = x in
+        {
+          Ast.Loc.source_name =
+            (match fname with None -> "(.)" | Some x -> x);
+          source_start = 0;
+          source_stop = 0;
+          line = start_line;
+          line_starts_at = start_col;
+        }
+
+end
+
+(** Terms.sym is exposed to Elpi as an opaque data type (no syntax like int or
+    string). APIs are provided to manipulate symbols, eg get their type *)
+let sym : Term.sym Conversion.t = OpaqueData.declare {
+  OpaqueData.name = "symbol";
+  doc = "A symbol";
+  pp = Print.sym;
+  compare = Term.Sym.compare;
+  hash = Hashtbl.hash;
+  hconsed = false;
+  constants = [];
+}
+
+(** Waiting for a ppx to do all the work for us, we code by hand the
+    conversion of Terms.term *)
+
+(* Allocate Elpi symbols for the term constructors (type and kind are Elpi
+   keywords, hence typ and kin) *)
+let typec = RawData.Constants.declare_global_symbol "typ"
+let kindc = RawData.Constants.declare_global_symbol "kin"
+let symbc = RawData.Constants.declare_global_symbol "symb"
+let prodc = RawData.Constants.declare_global_symbol "prod"
+let abstc = RawData.Constants.declare_global_symbol "abst"
+let applc = RawData.Constants.declare_global_symbol "appl"
+
+(* A two way map linking Elpi's unification variable and Terms.meta.
+   An instance of this map is part of the Elpi state (threaded by many
+   APIs) *)
+module M = struct
+  type t = Term.meta
+  let compare m1 m2 = Stdlib.compare m1.Term.meta_key m2.Term.meta_key
+  let pp = Print.meta
+  let show m = Format.asprintf "%a" pp m
+end
+module MM = FlexibleData.Map(M)
+let metamap : MM.t State.component = MM.uvmap
+
+let pb = State.declare ~name:"elpi:problem"
+  ~pp:(fun fmt (p : Term.problem) ->
+     Format.fprintf fmt "@[<hov 2>";
+     Term.MetaSet.iter (fun m ->
+       Format.fprintf fmt "%d@ " m.Term.meta_key) Timed.(! p).Term.metas;
+     Format.fprintf fmt "@]";
+  ) ~init:Term.new_problem ~start:(fun x -> x)
+
+
+(* Terms.term -> Data.term, we use Ctxt.ctxt to carry a link between
+   Bindlib's var to Elpi's De Bruijn levels *)
+let embed_term : ?pats:(int * string) list -> ?ctx:RawData.constant Term.actxt -> Term.term Conversion.embedding = fun ?(pats=[]) ?(ctx=[]) ~depth st t ->
+  let open RawData in
+  let open Term in
+  (*Common.Console.out 1 "BEFORE EMBED:@ %a@\n" Print.term t;*)
+  let gls = ref [] in
+  let call f ~depth s x =
+    let s, x, g = f ~depth s x in gls := g @ !gls; s, x in
+  let rec aux ~depth ctx st t =
+    (*Common.Console.out 1 "EMBED:@ %d |- %a@\n" (List.length ctx) Print.term t;*)
+    match Term.unfold t with
+    | Vari v ->
+
+        let d = Ctxt.type_of v ctx in
+        st, mkBound d
+    | Type -> st, mkGlobal typec
+    | Kind -> st, mkGlobal kindc
+    | Symb s ->
+        let st, s = call sym.Conversion.embed ~depth st s in
+        st, mkApp symbc s []
+    | Prod (src, tgt) ->
+        let st, src = aux ~depth ctx st src in
+        let _,tgt,ctx = Ctxt.unbind ~keep:true ctx depth None tgt in
+        let st, tgt = aux ~depth:(depth+1) ctx st tgt in
+        st, mkApp prodc src [mkLam tgt]
+    | Abst (ty, body) ->
+        let st, ty = aux ~depth ctx st ty in
+        let _,body,ctx = Ctxt.unbind ~keep:true ctx depth None body in
+        let st, body = aux ~depth:(depth+1) ctx st body in
+        st, mkApp prodc ty [mkLam body]
+    | Appl (hd, arg) ->
+        let st, hd = aux ~depth ctx st hd in
+        let st, arg = aux ~depth ctx st arg in
+        st, mkApp applc hd [arg]
+    | Meta (meta,args) ->
+        let st, flex =
+          try st, MM.elpi meta (State.get metamap st)
+          with Not_found ->
+            let st, flex = FlexibleData.Elpi.make st in
+            State.update metamap st (MM.add flex meta), flex in
+        let st, args = Elpi_AUX.array_map_fold (aux ~depth ctx) st args in
+        st, mkUnifVar flex ~args:(Array.to_list args) st
+    | Plac _ ->
+        let args = List.map (fun (_,x,_) -> mkBound x) ctx in
+        let st, flex = FlexibleData.Elpi.make st in
+        let st, meta = State.update_return pb st (fun pb ->
+          let m1 = LibMeta.fresh pb mk_Type 0 in
+          let m2 = LibMeta.fresh pb (mk_Meta (m1,[||]))
+            (List.length args) in (* empty context is surely wrong *)
+          pb, m2) in
+        let st = State.update metamap st (MM.add flex meta) in
+        st, mkUnifVar flex ~args st
+    | Patt(Some i,_,_) -> begin
+        try
+          let x = List.assoc i pats in
+          let st, flex = FlexibleData.Elpi.make ~name:x st in
+          st, mkUnifVar flex ~args:[] st
+        with Not_found ->
+          let pats = List.map (fun (i,n) -> Printf.sprintf "%d :-> %s; " i n) pats in
+          Common.Error.fatal_no_pos "embed_term: unnamed pattern %d in map: %s" i (String.concat "" pats);
+      end
+    | Patt _ -> Common.Error.fatal_no_pos "embed_term: Patt not implemented"
+    | TEnv _ -> Common.Error.fatal_no_pos "embed_term: TEnv not implemented"
+    | Wild   -> Common.Error.fatal_no_pos "embed_term: Wild not implemented"
+    | TRef _ -> Common.Error.fatal_no_pos "embed_term: TRef not implemented"
+    | LLet _ -> Common.Error.fatal_no_pos "embed_term: LLet not implemented"
+  in
+  let st, t = aux ~depth ctx st t in
+  st, t, List.rev !gls
+
+module IntMap = Map.Make(struct type t = int let compare = compare end)
+
+(* Data.term -> Terms.term. We use and IntMap to link Elpi's De Bruijn
+   levels to Bindlib's var *)
+let readback_term_box : Term.term Bindlib.box Conversion.readback =
+fun ~depth st t ->
+  let open RawData in
+  let open Term in
+  let gls = ref [] in
+  let call f ~depth s x =
+    let s, x, g = f ~depth s x in gls := g @ !gls; s, x in
+  let rec aux ~depth ctx st t =
+    match look ~depth t with
+    | Const c when c == typec -> st, _Type
+    | Const c when c == kindc -> st, _Kind
+    | Const c when c >= 0 ->
+        begin try
+          let v = IntMap.find c ctx in
+          st, _Vari v
+        with Not_found -> Utils.type_error "readback_term: free variable" end
+    | App(c,s,[]) when c == symbc ->
+        let st, s = call sym.Conversion.readback ~depth st s in
+        st, _Symb s
+    | App(c,ty,[bo]) when c == prodc ->
+        let st, ty = aux ~depth ctx st ty in
+        let st, bo = aux_lam ~depth ctx st bo in
+        st, _Prod ty bo
+    | App(c,ty,[bo]) when c == abstc ->
+        let st, ty = aux ~depth ctx st ty in
+        let st, bo = aux_lam ~depth ctx st bo in
+        st, _Abst ty bo
+    | App(c,hd,[arg]) when c == applc ->
+        let st, hd = aux ~depth ctx st hd in
+        let st, arg = aux ~depth ctx st arg in
+        st, _Appl hd arg
+    | UnifVar(flex, args) ->
+        let st, meta =
+          try st, MM.host flex (State.get metamap st)
+          with Not_found ->
+            let st, m2 = State.update_return pb st (fun pb ->
+              let m1 = LibMeta.fresh pb mk_Type 0 in
+              let m2 = LibMeta.fresh pb (mk_Meta (m1,[||]))
+                (List.length args) in (* empty context is surely wrong *)
+              pb, m2) in
+            State.update metamap st (MM.add flex m2), m2
+           in
+        let st, args = Elpi_AUX.list_map_fold (aux ~depth ctx) st args in
+        st, _Meta meta (Array.of_list args)
+    | _ -> Utils.type_error "readback_term"
+  and aux_lam ~depth ctx st t =
+    match look ~depth t with
+    | Lam bo ->
+        let v = Bindlib.new_var of_tvar "x" in
+        let ctx = IntMap.add depth v ctx in
+        let st, bo = aux ~depth:(depth+1) ctx st bo in
+        st, Bindlib.bind_var v bo
+    | _ -> Utils.type_error "readback_term"
+  in
+  let st, t = aux ~depth IntMap.empty st t in
+  st, t, List.rev !gls
+
+let readback_term ~depth st t =
+  let st, t, gls = readback_term_box ~depth st t in
+  st, Bindlib.unbox t, gls
+
+(** Terms.term has a HOAS *)
+let term : Term.term Conversion.t = {
+  Conversion.ty = Conversion.TyName "term";
+  pp = Print.term;
+  pp_doc = (fun fmt () -> Format.fprintf fmt {|
+kind term type.
+type typ term.
+type kin term.
+type symb symbol -> term.
+type appl term -> term -> term.
+type abst term -> (term -> term) -> term.
+type prod term -> (term -> term) -> term.
+  |});
+  readback = readback_term;
+  embed = embed_term ?ctx:None ?pats:None;
+}
+
+(** Assignments to Elpi's unification variables are a spine of lambdas
+    followed by an actual term. We read them back as a Bindlib.mbinder *)
+let readback_mbinder st t =
+  let open RawData in
+  let rec aux ~depth nvars t =
+    match look ~depth t with
+    | Lam bo -> aux ~depth:(depth+1) (nvars+1) bo
+    | _ ->
+        let open Bindlib in
+        let vs = Array.init nvars (fun i ->
+          new_var Term.of_tvar (Printf.sprintf "x%d" i)) in
+        let st, t, _ = readback_term_box ~depth st t in
+        st, unbox (bind_mvar vs t)
+  in
+    aux ~depth:0 0 t
+let readback_assignments st =
+  let mmap = State.get metamap st in
+  MM.fold (fun meta _flex body st ->
+    match body with
+    | None -> st
+    | Some t ->
+        let open Timed in
+        match ! (meta.Term.meta_value) with
+        | Some _ -> assert false
+        | None ->
+            let st, t = readback_mbinder st t in
+            meta.Term.meta_value := Some t;
+            st
+    ) mmap st
+
diff --git a/src/core/sig_state.ml b/src/core/sig_state.ml
index 4d1e8cca4..a031562c5 100644
--- a/src/core/sig_state.ml
+++ b/src/core/sig_state.ml
@@ -30,8 +30,10 @@ type sig_state =
   ; path_alias: string Path.Map.t         (** Path to alias map. *)
   ; builtins  : sym StrMap.t              (** Builtins. *)
   ; notations : float notation SymMap.t   (** Notations. *)
-  ; open_paths : Path.Set.t               (** Open modules. *) }
-
+  ; open_paths : Path.Set.t               (** Open modules. *)
+  ; active_tc       : SymSet.t            (** Active TC *)
+  ; active_tc_inst  : SymSet.t            (** Active TC instances *)
+  }
 type t = sig_state
 
 (** Dummy [sig_state]. *)
@@ -39,25 +41,33 @@ let dummy : sig_state =
   { signature = Sign.dummy (); in_scope = StrMap.empty;
     alias_path = StrMap.empty; path_alias = Path.Map.empty;
     builtins = StrMap.empty; notations = SymMap.empty;
-    open_paths = Path.Set.empty }
+    open_paths = Path.Set.empty;
+    active_tc = SymSet.empty;
+    active_tc_inst = SymSet.empty;
+  }
 
-(** [add_symbol ss expo prop mstrat opaq id typ impl def] generates a new
+(** [add_symbol ss expo prop mstrat opaq id typ impl tc def] generates a new
    signature state from [ss] by creating a new symbol with expo [e], property
    [p], strategy [st], name [x], type [a], implicit arguments [impl] and
    optional definition [def]. This new symbol is returned too. *)
 let add_symbol : sig_state -> expo -> prop -> match_strat
-    -> bool -> strloc -> term -> bool list -> term option -> sig_state * sym =
-  fun ss expo prop mstrat opaq id typ impl def ->
+    -> bool -> strloc -> term -> bool list -> bool -> bool -> term option ->
+      sig_state * sym =
+  fun ss expo prop mstrat opaq id typ impl tc tci def ->
   let sym =
     Sign.add_symbol ss.signature expo prop mstrat opaq id
       (cleanup typ) impl in
+  if tc then Sign.add_tc ss.signature sym;
+  let active_tc = if tc then SymSet.add sym ss.active_tc else ss.active_tc in
+  if tci then Sign.add_tc_inst ss.signature sym;
+  let active_tc_inst = if tci then SymSet.add sym ss.active_tc_inst else ss.active_tc_inst in
   begin
     match def with
     | Some t -> sym.sym_def := Some (cleanup t)
     | None -> ()
   end;
   let in_scope = StrMap.add id.elt sym ss.in_scope in
-  {ss with in_scope}, sym
+  {ss with in_scope; active_tc; active_tc_inst}, sym
 
 (** [add_notation ss s n] maps [s] notation to [n] in [ss]. *)
 let add_notation : sig_state -> sym -> float notation -> sig_state =
@@ -87,6 +97,13 @@ let open_sign : sig_state -> Sign.t -> sig_state = fun ss sign ->
   let open_paths = Path.Set.add sign.sign_path ss.open_paths in
   {ss with in_scope; builtins; notations; open_paths}
 
+let open_sign_tc : sig_state -> Sign.t -> sig_state = fun ss sign ->
+  Common.Console.out 1 "ACTIVATING %d classes." (SymSet.cardinal !(sign.sign_tc_inst));
+  { ss with 
+      active_tc = SymSet.union ss.active_tc !(sign.sign_tc);
+      active_tc_inst = SymSet.union ss.active_tc_inst !(sign.sign_tc_inst);
+  }
+
 (** [of_sign sign] creates a state from the signature [sign] and open it as
    well as the ghost signatures. *)
 let of_sign : Sign.t -> sig_state = fun signature ->
diff --git a/src/core/sign.ml b/src/core/sign.ml
index a40db549d..0c474724f 100644
--- a/src/core/sign.ml
+++ b/src/core/sign.ml
@@ -36,6 +36,8 @@ type t =
   ; sign_notations: float notation SymMap.t ref
   (** Maps symbols to their notation if they have some. *)
   ; sign_ind      : ind_data SymMap.t ref
+  ; sign_tc       : SymSet.t ref
+  ; sign_tc_inst  : SymSet.t ref
   ; sign_cp_pos   : cp_pos list SymMap.t ref
   (** Maps a symbol to the critical pair positions it is heading in the
      rules. *) }
@@ -51,6 +53,7 @@ let dummy : unit -> t = fun () ->
   { sign_symbols = ref StrMap.empty; sign_path = []
   ; sign_deps = ref Path.Map.empty; sign_builtins = ref StrMap.empty
   ; sign_notations = ref SymMap.empty; sign_ind = ref SymMap.empty
+  ; sign_tc = ref SymSet.empty; sign_tc_inst = ref SymSet.empty
   ; sign_cp_pos = ref SymMap.empty }
 
 (** [find sign name] finds the symbol named [name] in [sign] if it exists, and
@@ -265,6 +268,8 @@ let read : string -> t = fun fname ->
   unsafe_reset sign.sign_notations;
   unsafe_reset sign.sign_ind;
   unsafe_reset sign.sign_cp_pos;
+  unsafe_reset sign.sign_tc;
+  unsafe_reset sign.sign_tc_inst;
   let shallow_reset_sym s =
     unsafe_reset s.sym_type;
     unsafe_reset s.sym_def;
@@ -301,6 +306,8 @@ let read : string -> t = fun fname ->
   StrMap.iter (fun _ s -> reset_sym s) !(sign.sign_symbols);
   StrMap.iter (fun _ s -> shallow_reset_sym s) !(sign.sign_builtins);
   SymMap.iter (fun s _ -> shallow_reset_sym s) !(sign.sign_notations);
+  SymSet.iter (fun s -> reset_sym s) !(sign.sign_tc);
+  SymSet.iter (fun s -> reset_sym s) !(sign.sign_tc_inst);
   let f _ sm = StrMap.iter (fun _ rs -> List.iter reset_rule rs) sm in
   Path.Map.iter f !(sign.sign_deps);
   let reset_ind i =
@@ -413,3 +420,12 @@ let rec dependencies : t -> (Path.t * t) list = fun sign ->
     | d::deps -> minimize ((List.filter not_here d) :: acc) deps
   in
   List.concat (minimize [] deps)
+
+let add_tc : t -> sym -> unit =
+  fun sign sym ->
+    sign.sign_tc := SymSet.add sym !(sign.sign_tc)
+
+let add_tc_inst : t -> sym -> unit =
+  fun sign sym ->    
+    sign.sign_tc_inst := SymSet.add sym !(sign.sign_tc_inst);
+  
diff --git a/src/core/term.ml b/src/core/term.ml
index 332f3781e..3981c3159 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -275,7 +275,8 @@ end
     list [xn:An;..;x1:A1] in reverse order (last added variable comes
     first). Note that it cannot be implemented by a map as the order is
     important. *)
-type ctxt = (tvar * term * term option) list
+type 'a actxt = (tvar * 'a * term option) list
+type ctxt = term actxt
 
 (** Typing context with lifted terms. Used to optimise type checking and avoid
     lifting terms several times. Definitions are not included because these
@@ -350,7 +351,7 @@ type problem = problem_aux ref
 let new_problem : unit -> problem = fun () ->
  ref {to_solve  = []; unsolved = []; recompute = false; metas = MetaSet.empty}
 
-(** [create_sym path expo prop opaq name typ impl] creates a new symbol with
+(** [create_sym path expo prop opaq name typ impl tc] creates a new symbol with
    path [path], exposition [expo], property [prop], opacity [opaq], matching
    strategy [mstrat], name [name.elt], type [typ], implicit arguments [impl],
    position [name.pos], no definition and no rules. *)
diff --git a/src/core/term.mli b/src/core/term.mli
index cbf5d1dfb..6cdcac610 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -256,7 +256,8 @@ end
     definition. The typing environment [x1:A1,..,xn:An] is represented by the
     list [xn:An;..;x1:A1] in reverse order (last added variable comes
     first). *)
-type ctxt = (tvar * term * term option) list
+type 'a actxt = (tvar * 'a * term option) list
+type ctxt = term actxt
 
 (** Typing context with lifted terms. Used to optimise type checking and avoid
     lifting terms several times. Definitions are not included because these
@@ -293,10 +294,11 @@ module Sym : Map.OrderedType with type t = sym
 module SymSet : Set.S with type elt = sym
 module SymMap : Map.S with type key = sym
 
-(** [create_sym path expo prop opaq name typ impl] creates a new symbol with
+(** [create_sym path expo prop opaq name typ impl tc] creates a new symbol with
    position [pos], path [path], exposition [expo], property [prop], opacity
    [opaq], matching strategy [mstrat], name [name.elt], type [typ], implicit
-   arguments [impl], position [name.pos], no definition and no rules. *)
+   arguments [impl], position [name.pos], typeclass [tc] no definition and no
+   rules. *)
 val create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
   Pos.strloc -> term -> bool list -> sym
 
diff --git a/src/core/unif_rule.ml b/src/core/unif_rule.ml
index eb2b73f89..1a9972201 100644
--- a/src/core/unif_rule.ml
+++ b/src/core/unif_rule.ml
@@ -10,13 +10,15 @@ open Term
 (** Symbol "≡". *)
 let equiv : sym =
   let id = Pos.none "≡" in
-  let s = Sign.add_symbol Ghost.sign Public Defin Eager false id mk_Kind [] in
+  let s =
+    Sign.add_symbol Ghost.sign Public Defin Eager false id mk_Kind [] in
   Sign.add_notation Ghost.sign s (Infix(Pratter.Neither, 2.0)); s
 
 (** Symbol ";". *)
 let cons : sym =
   let id = Pos.none ";" in
-  let s = Sign.add_symbol Ghost.sign Public Const Eager true id mk_Kind [] in
+  let s =
+    Sign.add_symbol Ghost.sign Public Const Eager true id mk_Kind [] in
   Sign.add_notation Ghost.sign s (Infix(Pratter.Right, 1.0)); s
 
 (** [unpack eqs] transforms a term of the form
diff --git a/src/export/coq.ml b/src/export/coq.ml
index c7b86cdf8..86d8a7185 100644
--- a/src/export/coq.ml
+++ b/src/export/coq.ml
@@ -55,6 +55,8 @@ let modifier : p_modifier pp = fun ppf {elt; _} ->
   | P_mstrat(s) -> Print.match_strat ppf s
   | P_prop(p)   -> Print.prop ppf p
   | P_opaq      -> out ppf "opaque "
+  | P_typeclass -> assert false (* TODO *)
+  | P_typeclass_instance -> assert false (* TODO *)
 
 (* ends with a space if the list is not empty *)
 let modifiers : p_modifier list pp = List.pp modifier ""
@@ -247,7 +249,7 @@ let command : p_command pp = fun ppf { elt; _ } ->
         (List.pp (inductive "and") "@,") il
   | P_notation (qid, n) ->
     out ppf "(*Notation %a %a.*)@." qident qid notation n
-  | P_open ps -> out ppf "Import %a@." (List.pp path " ") ps
+  | P_open(_,ps) -> out ppf "Import %a@." (List.pp path " ") ps
   | P_query _ -> ()
   | P_require (b, ps) ->
       out ppf "Require%a %a.@."
@@ -271,6 +273,9 @@ let command : p_command pp = fun ppf { elt; _ } ->
         (Option.pp (unit "@," |+ proof)) p_sym_prf
     end
   | P_unif_rule _ -> ()
+  | P_elpi _ -> ()
+  | P_type_class( { Pos.elt = id; _ } ) -> out ppf "Existing Class %s. " id
+  | P_type_class_instance( { Pos.elt = id; _ } ) -> out ppf "Existing Instance %s. " id
   end
 
 let ast : ast pp = fun ppf -> Stream.iter (command ppf)
diff --git a/src/export/dk.ml b/src/export/dk.ml
index 28a7fa2ef..2a6c68ef5 100644
--- a/src/export/dk.ml
+++ b/src/export/dk.ml
@@ -239,4 +239,6 @@ let require : Path.t -> _ -> unit = fun p _ ->
 let sign : Sign.t -> unit = fun sign ->
   Path.Map.iter require !(sign.sign_deps);
   Stdlib.(current_path := sign.sign_path);
-  List.iter (decl Format.std_formatter) (decls_of_sign sign)
+  List.iter (decl Format.std_formatter) (decls_of_sign sign);
+  SymSet.iter (fun symb -> Format.printf "#TYPE_CLASS %s.\n" symb.sym_name) !(sign.sign_tc);
+  SymSet.iter (fun symb -> Format.printf "#TYPE_CLASS_INSTANCE %s.\n" symb.sym_name) !(sign.sign_tc_inst)
diff --git a/src/handle/command.ml b/src/handle/command.ml
index 07924450b..6dca5eddc 100644
--- a/src/handle/command.ml
+++ b/src/handle/command.ml
@@ -50,6 +50,19 @@ let handle_open : sig_state -> p_path -> sig_state =
   (* Obtain the signature corresponding to [p]. *)
   open_sign ss (Path.Map.find p !(Sign.loaded))
 
+let handle_open_tc : sig_state -> p_path -> sig_state =
+  fun ss {elt=p;pos} ->
+  (* Check that [p] is not an alias. *)
+  match p with
+  | [a] when StrMap.mem a ss.alias_path ->
+    fatal pos "Module aliases cannot be open."
+  | _ ->
+  (* Check that [p] has been required. *)
+  if not (Path.Map.mem p !(ss.signature.sign_deps)) then
+    fatal pos "Module %a needs to be required first." path p;
+  (* Obtain the signature corresponding to [p]. *)
+  open_sign_tc ss (Path.Map.find p !(Sign.loaded))
+
 (** [handle_require b ss p] handles the command [require p] (or [require
    open p] if b is true) with [ss] as the signature state and [compile] the
    main compile function (passed as argument to avoid cyclic dependencies).
@@ -80,17 +93,19 @@ let handle_require_as : compiler -> sig_state -> p_path -> p_ident ->
 
 (** [handle_modifiers ms] verifies that the modifiers in [ms] are compatible.
     If so, they are returned as a tuple. Otherwise, it fails. *)
-let handle_modifiers : p_modifier list -> prop * expo * match_strat =
+let handle_modifiers : p_modifier list -> prop * expo * match_strat * bool * bool =
   fun ms ->
-  let rec get_modifiers ((props, expos, strats) as acc) = function
+  let rec get_modifiers ((props, expos, strats,tc,tci) as acc) = function
     | [] -> acc
-    | {elt=P_prop _;_} as p::ms -> get_modifiers (p::props, expos, strats) ms
-    | {elt=P_expo _;_} as e::ms -> get_modifiers (props, e::expos, strats) ms
+    | {elt=P_typeclass;_}::ms -> get_modifiers (props, expos, strats,true, tci) ms
+    | {elt=P_typeclass_instance;_}::ms -> get_modifiers (props, expos, strats,tc, true) ms
+    | {elt=P_prop _;_} as p::ms -> get_modifiers (p::props, expos, strats,tc,tci) ms
+    | {elt=P_expo _;_} as e::ms -> get_modifiers (props, e::expos, strats,tc,tci) ms
     | {elt=P_mstrat _;_} as s::ms ->
-        get_modifiers (props, expos, s::strats) ms
+        get_modifiers (props, expos, s::strats,tc,tci) ms
     | {elt=P_opaq;_}::ms -> get_modifiers acc ms
   in
-  let props, expos, strats = get_modifiers ([],[],[]) ms in
+  let props, expos, strats, tc, tci = get_modifiers ([],[],[],false,false) ms in
   let prop =
     match props with
     | [{elt=P_prop (Assoc b);_};{elt=P_prop Commu;_}]
@@ -119,7 +134,7 @@ let handle_modifiers : p_modifier list -> prop * expo * match_strat =
     | [] -> Eager
     | _ -> assert false
   in
-  (prop, expo, strat)
+  (prop, expo, strat, tc, tci)
 
 (** [check_rule ss syms r] checks rule [r] and returns the head symbol of the
    lhs and the rule itself. *)
@@ -163,7 +178,8 @@ let handle_inductive_symbol : sig_state -> expo -> prop -> match_strat
   end;
   (* Actually add the symbol to the signature and the state. *)
   Console.out 2 (Color.red "symbol %a : %a") uid name term typ;
-  let r = Sig_state.add_symbol ss expo prop mstrat false id typ impl None in
+  let r =
+    Sig_state.add_symbol ss expo prop mstrat false id typ impl false false None in
   sig_state := fst r; r
 
 (** Representation of a yet unchecked proof. The structure is initialized when
@@ -195,11 +211,23 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   Console.out 3 (Color.cya "%a") Pos.pp pos;
   Console.out 4 "%a" Pretty.command cmd;
   match elt with
+  | P_type_class({ Pos.elt = id; pos }) ->
+    let sym = Sig_state.find_sym ~prt:false ~prv:false ss { Pos.elt = ([],id); pos} in
+    Sign.add_tc ss.signature sym;
+    { ss with Sig_state.active_tc = SymSet.add sym ss.active_tc }, None, None
+  | P_type_class_instance ({ Pos.elt = id; pos }) ->
+    let sym = Sig_state.find_sym ~prt:false ~prv:false ss { Pos.elt = ([],id); pos} in
+    Sign.add_tc_inst ss.signature sym;
+    { ss with Sig_state.active_tc_inst = SymSet.add sym ss.active_tc_inst }, None, None
+  | P_elpi(file,pred,arg) ->
+      (ss, None, (Elpi_handle.run ss file pred arg; None))
   | P_query(q) -> (ss, None, Query.handle ss None q)
   | P_require(b,ps) ->
       (List.fold_left (handle_require compile b) ss ps, None, None)
   | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None)
-  | P_open(ps) -> (List.fold_left handle_open ss ps, None, None)
+  | P_open([],ps) -> (List.fold_left handle_open ss ps, None, None)
+  | P_open(["tc"],ps) -> (List.fold_left handle_open_tc ss ps, None, None)
+  | P_open _ -> fatal pos "only \"tc\" filter implemented"
   | P_rules(rs) ->
     (* Scope rules, and check that they preserve typing. Return the list of
        rules [srs] and also a map [map] mapping every symbol defined by a rule
@@ -286,7 +314,11 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
 
   | P_inductive(ms, params, p_ind_list) ->
       (* Check modifiers. *)
-      let (prop, expo, mstrat) = handle_modifiers ms in
+      let (prop, expo, mstrat,tc,tci) = handle_modifiers ms in
+      if tc then
+        fatal pos "Property typeclass cannot be used on inductive types.";
+      if tci then
+        fatal pos "Property instance cannot be used on inductive types.";
       if prop <> Defin then
         fatal pos "Property modifiers cannot be used on inductive types.";
       if mstrat <> Eager then
@@ -354,7 +386,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
           let pos = after (end_pos pos) in
           let id = Pos.make pos rec_name in
           let r =
-            Sig_state.add_symbol ss expo Defin Eager false id rec_typ [] None
+            Sig_state.add_symbol
+              ss expo Defin Eager false id rec_typ [] false false None
           in sig_state := fst r; r
         in
         (ss, rec_sym::rec_sym_list)
@@ -392,7 +425,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       | _ -> ()
     end;
     (* Verify modifiers. *)
-    let prop, expo, mstrat = handle_modifiers p_sym_mod in
+    let prop, expo, mstrat, tc, tci = handle_modifiers p_sym_mod in
     let opaq = List.exists Syntax.is_opaq p_sym_mod in
     let pdata_prv = expo = Privat || (p_sym_def && opaq) in
     (match p_sym_def, opaq, prop, mstrat with
@@ -495,18 +528,18 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
             wrn pe.pos "Proof admitted.";
             let t = Option.map (fun t -> t.elt) t in
             fst (Sig_state.add_symbol
-                   ss expo prop mstrat opaq p_sym_nam a impl t)
+                   ss expo prop mstrat opaq p_sym_nam a impl tc tci t)
         | P_proof_end ->
             (* Check that the proof is indeed finished. *)
             if not (finished ps) then
-              fatal pe.pos "The proof is not finished.";
+              fatal pe.pos "The proof is not finished.@.%a" goals ps;
             (* Get the final definition. *)
             let d =
               Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term in
             (* Add the symbol in the signature. *)
             Console.out 2 (Color.red "symbol %a : %a") uid id term a;
             fst (Sig_state.add_symbol
-                   ss expo prop mstrat opaq p_sym_nam a impl d)
+                   ss expo prop mstrat opaq p_sym_nam a impl tc tci d)
       in
       (* Create the proof state. *)
       let pdata_state =
@@ -554,8 +587,10 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   | Fatal(Some(Some(_)),_) as e -> raise e
   | Fatal(None         ,m)      -> fatal pos "Error on command.@.%s" m
   | Fatal(Some(None)   ,m)      -> fatal pos "Error on command.@.%s" m
+  (*
   | e                           ->
       fatal pos "Uncaught exception: %s." (Printexc.to_string e)
+*)
 
 (** [handle compile_mod ss cmd] retrieves proof data from [cmd] (with
     {!val:get_proof_data}) and handles proofs using functions from
diff --git a/src/handle/dune b/src/handle/dune
index 05be56087..8703f3f57 100644
--- a/src/handle/dune
+++ b/src/handle/dune
@@ -2,4 +2,4 @@
  (name handle)
  (public_name lambdapi.handle)
  (modules :standard)
- (libraries lambdapi.core lambdapi.parsing lambdapi.tool))
+ (libraries lambdapi.core lambdapi.parsing lambdapi.tool elpi))
diff --git a/src/handle/elpi_handle.ml b/src/handle/elpi_handle.ml
new file mode 100644
index 000000000..2b71bcfc9
--- /dev/null
+++ b/src/handle/elpi_handle.ml
@@ -0,0 +1,316 @@
+open Elpi.API
+open Core
+open Elpi_lambdapi
+
+let ss : Sig_state.t State.component =
+  State.declare ~name:"elpi:ss"
+    ~pp:(fun _fmt _ -> ()) ~init:(fun () -> Sig_state.dummy) ~start:(fun x -> x)
+
+let goalc = RawData.Constants.declare_global_symbol "goal"
+let ofc = RawData.Constants.declare_global_symbol "of"
+let nablac = RawData.Constants.declare_global_symbol "nabla"
+let sealc = RawData.Constants.declare_global_symbol "seal"
+
+let embed_goal : Term.meta Conversion.embedding = fun ~depth st m ->
+  let open Term in
+  let ty =
+    let open Timed in
+    !(m.meta_type) in 
+
+  let open RawData in
+  let open Utils in
+  (*Common.Console.out 1 "BEFORE EMBED GOAL:@ %a@\n" Print.term ty;*)
+
+  let rec aux ~depth st (c,ctx,i,args) ty =
+    match unfold ty with
+    | Prod (dom,b) ->
+      (*Common.Console.out 1 "EMBED HYP:@ %a@\n" Print.term dom;*)
+      let st, dom, gls = embed_term ~ctx:c ~depth st dom in
+      let x,b,c = Ctxt.unbind ~keep:true c depth None b in
+      let st, g, gls1 =
+        aux ~depth:(depth+1) st
+          (c,(depth+1,mkApp ofc (mkBound depth) [dom])::ctx,i,x::args) b in
+      st, mkApp nablac (mkLam g) [], gls @ gls1
+    | _ ->
+       (*Common.Console.out 1 "EMBED CONCL:@ %d %d |- %a@\n" (List.length c) (List.length ctx) Print.term ty;*)
+       let ctx = List.map (fun (from,t) -> move ~from ~to_:depth t) ctx in
+       let st, ty, gls = embed_term ~ctx:c ~depth st ty in
+       let args = List.rev args |> List.map Term.of_tvar in
+       let args1,args2 = Lplib.List.cut args (i.Term.meta_arity) in
+       let m = Term.add_args (mk_Meta (i, args1 |> Array.of_list)) args2 in
+       let st, i, gls1 = embed_term ~ctx:c ~depth st m in
+       st, mkApp sealc (mkApp goalc (list_to_lp_list ctx) [ty; i]) [], gls @ gls1
+  in
+  let rc = aux ~depth st ([],[],m,[]) ty in
+  (*Common.Console.out 1 "EMBED GOAL END ------------:@ %a@\n" Print.term ty;*)
+  rc
+   
+let goal : Term.meta Conversion.t = {
+  Conversion.embed = embed_goal;
+  readback = (fun ~depth:_ _ _ -> assert false);
+  pp_doc = (fun fmt _ -> Format.fprintf fmt "TODO");
+  pp = (fun fmt _ -> Format.fprintf fmt "TODO");
+  ty = Conversion.TyName "sealed-goal"
+}
+
+(** APIs (data types and predicates) exposed to Elpi *)
+let lambdapi_builtin_declarations : BuiltIn.declaration list =
+  let open BuiltIn in
+  let open BuiltInPredicate in
+  let open BuiltInData in
+  let open BuiltInPredicate.Notation in
+[
+  LPDoc "---- Lambdapi datatypes ----";
+
+  MLData sym;
+  MLData term;
+  LPCode {|
+kind sealed-goal type.
+type nabla (term -> sealed-goal) -> sealed-goal.
+type seal goal -> sealed-goal.
+
+kind goal type.
+type goal list prop -> term -> term -> goal.
+
+type of term -> term -> prop.
+
+pred msolve o:list sealed-goal.
+  
+|};
+
+  LPDoc "---- Builtin predicates ----";
+
+  MLCode(Pred("lp.sig",
+    In(sym,"S",
+    Out(term,"T",
+    Easy "Gives the type of a symbol")),
+    (fun s _ ~depth:_ -> !: (Timed.(!) s.Term.sym_type))),
+    DocAbove);
+
+  MLCode(Pred("lp.tc-instances",
+    Out(list sym,"L",
+    Read (ContextualConversion.unit_ctx, "Gives the list of type class instances")),
+    (fun _ ~depth:_ _ _ state ->
+      let s = State.get ss state in
+      !: (s.Sig_state.active_tc_inst |> Term.SymSet.elements))),
+    DocAbove);
+
+  MLCode(Pred("lp.tc?",
+    In(sym,"S",
+    Read (ContextualConversion.unit_ctx, "Tells if S is a type class")),
+    (fun sym ~depth:_ _ _ state ->
+      let s = State.get ss state in
+      if (s.Sig_state.active_tc |> Term.SymSet.mem sym) then ()
+      else raise No_clause)),
+    DocAbove);
+
+  MLCode(Pred("lp.snf",
+    In(term,"X",
+    Out(term,"SX",
+    Read (ContextualConversion.unit_ctx, "SX is the snf of X"))),
+    (fun t _ ~depth:_ _ _ _ ->
+      !: (Eval.snf ~tags:[`NoExpand] [] t))),
+    DocAbove);
+
+  MLCode(Pred("lp.eq_modulo",
+    In(term,"X",
+    In(term,"Y",
+    Read (ContextualConversion.unit_ctx, "X = Y upto rewrite"))),
+    (fun x y ~depth:_ _ _ _ ->
+      if Eval.pure_eq_modulo [] x y then () else raise No_clause)),
+    DocAbove);
+
+  MLCode(Pred("lp.unif",
+    In(term,"X",
+    In(term,"Y",
+    Read (ContextualConversion.unit_ctx, "unify X with Y"))),
+    (fun x y ~depth:_ _ _ state ->
+      let problem = State.get pb state in
+      let open Timed in
+      (* CSC: empty context is bad here *)
+      Common.Console.out 1 "\n***UNIF before: %a == %a\n" Print.term x Print.term y;
+      assert (List.length !problem.Term.unsolved = 0);
+      problem := Term.{ !problem with to_solve = ([],x,y)::!problem.to_solve } ;
+      if Unif.solve_noexn problem then begin
+       assert (List.length !problem.Term.unsolved = 0);
+       Common.Console.out 1 "\n***UNIF after: %a == %a\n" Print.term x Print.term y;
+       ()
+      end else raise No_clause)),
+    DocAbove);
+
+  MLCode(Pred("lp.term->string",
+    In(term,"T",
+    Out(string,"S",
+    Easy "Pretty prints a term T to the string S")),
+    (fun t _ ~depth:_ -> !: (Format.asprintf "%a" Print.term t))),
+    DocAbove);
+
+  LPDoc "---- Elpi predicates ----";
+
+] @ Elpi.Builtin.std_declarations
+
+let lambdapi_builtins =
+  BuiltIn.declare ~file_name:"lambdap.elpi" lambdapi_builtin_declarations
+
+let document () =
+  BuiltIn.document_file ~header:"% automatically generated" lambdapi_builtins
+
+(** The runtime of Elpi (we need only one I guess) *)
+let elpi = ref None
+
+let init () =
+  let e = Setup.init
+    ~builtins:[lambdapi_builtins]
+    ~legacy_parser:false
+    ~file_resolver:(Parse.std_resolver ~paths:[] ()) () in
+  elpi := Some e;
+  document ()
+
+(** Given an Elpi file, a predicate name and a Terms.term argument we
+    run Elpi and print the term before/after the execution  *)
+let run : Sig_state.t -> string -> string -> Parsing.Syntax.p_term -> unit =
+fun ss file predicate arg ->
+  let pos = arg.Common.Pos.pos in
+  let loc = Elpi_AUX.loc_of_pos pos in
+  let arg = Parsing.Scope.scope_term false ss Env.empty arg in
+  let elpi = match !elpi with None -> assert false | Some x -> x in
+
+  let ast = Parse.program ~elpi ~files:[file] in
+  let prog =
+    let flags = Elpi.API.Compile.default_flags in
+    ast |>
+    Elpi.API.Compile.unit ~flags ~elpi |>
+    (fun u -> Elpi.API.Compile.assemble ~elpi ~flags [u]) in
+
+  let query =
+    let open Elpi.API.Query in
+    compile prog loc
+      (Query { predicate; arguments = (D(term,arg,Q(term,"it",N))) }) in
+
+  if not (Elpi.API.Compile.static_check
+            ~checker:(Elpi.Builtin.default_checker ()) query) then
+    Common.Error.fatal pos "elpi: type error in %s" file;
+
+  Common.Console.out 1 "\nelpi: before: %a\n" Print.term arg;
+  match Execute.once (Elpi.API.Compile.optimize query) with
+  | Execute.Success {
+      Data.state; pp_ctx; constraints; output = (arg1,()); _
+    } ->
+      let _ = readback_assignments state in
+      Common.Console.out 1 "\nelpi: after: %a\n" Print.term arg1;
+      Common.Console.out 1 "elpi: constraints:@ @[<v>%a@]\n"
+        Pp.(constraints pp_ctx) constraints
+  | Failure -> Common.Error.fatal_no_pos "elpi: failure"
+  | NoMoreSteps -> assert false
+
+let extend (cctx) v ?def ty = (v, ty, def) :: cctx
+
+let is_tc_instance : Sig_state.t -> Term.ctxt -> Term.meta -> bool =
+  fun ss c m ->
+  let open Timed in
+  let open Term in
+  let is_tc symb  =
+    SymSet.mem symb !(ss.Sig_state.signature.Sign.sign_tc) in
+  let rec aux c t =
+    match get_args (unfold t) with
+    | Symb s, _ -> is_tc s
+    | Prod(dom, b), [] ->
+      let (x, b) = Bindlib.unbind b in
+      let c = extend c x dom in
+      aux c b
+    | _ -> false
+  in
+    aux c !(m.meta_type)
+
+let metas_of_term : Term.ctxt -> Term.term -> Term.meta list =
+  fun c t ->
+  let open Term in
+  let acc = ref [] in
+  let rec aux c t =
+    match unfold t with
+    | Meta(m,_) when not (List.memq m !acc) ->
+       acc := m :: !acc
+    | Abst (dom, b) | Prod(dom, b) ->
+       aux c dom;
+       let (x, b) = Bindlib.unbind b in
+       let c = extend c x dom in
+       aux c b
+    | LLet (dom, t, b) ->
+       aux c dom;
+       aux c t;
+       let (x, b) = Bindlib.unbind b in
+       let c = extend c x dom in
+       aux c b
+    | Appl(t,u) -> aux c t; aux c u
+    | Plac _ -> assert false (* term was inferred before *)
+    | _ -> ()
+  in
+    aux c t;
+    !acc
+
+
+let scope_ref : (Parsing.Syntax.p_term -> Term.term * (int * string) list) ref = ref (fun _ -> assert false)
+
+(* we set the state, Elpi.API.Qery lacks this function *)
+let hack s c = { c with Conversion.embed =
+  fun ~depth state x ->
+    let state = State.set ss state s in
+    c.Conversion.embed ~depth state x
+}
+
+let solve_tc : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list) -> Sig_state.t -> Common.Pos.popt -> Term.problem -> Term.ctxt ->
+  Term.term * Term.term -> Term.term * Term.term =
+  fun ?scope ss pos _pb ctxt (t,ty) ->
+    let tc = metas_of_term ctxt t in
+    if tc <> [] then begin
+      let elpi = match !elpi with None -> assert false | Some x -> x in
+      Option.iter (fun f -> scope_ref := f) scope;
+
+      Common.Console.out 1 "BEFORE TC RESOLUTION:@ %a : %a@\n" Print.term t Print.term ty;
+      List.iter
+        (fun m ->
+          Common.Console.out 1 "META TY:@ %d : %a@\n" m.Term.meta_key Print.term (Timed.(!(m.Term.meta_type))))
+          tc;
+
+      let file = "tcsolver.elpi" in
+      let predicate = "msolve" in
+      let pos = Elpi_AUX.loc_of_pos pos in
+
+      let ast = Parse.program ~elpi ~files:[file] in
+      let prog =
+        let flags = Elpi.API.Compile.default_flags in
+        ast |>
+        Elpi.API.Compile.unit ~flags ~elpi |>
+        (fun u -> Elpi.API.Compile.assemble ~elpi ~flags [u]) in
+    
+      let query =
+        let open Elpi.API.Query in
+        let open Elpi.API.BuiltInData in
+        compile prog pos
+          (Query { predicate; arguments = (D(hack ss (list goal),tc,N)) }) in
+    
+      if not (Elpi.API.Compile.static_check
+                ~checker:(Elpi.Builtin.default_checker ()) query) then
+        Common.Console.out 1 "elpi: type error in %s" file;
+    
+      match Execute.once (Elpi.API.Compile.optimize query) with
+      | Execute.Success { Data.state; output = (); _ } ->
+          let _ = readback_assignments state in
+          ()
+      | Failure -> Common.Error.fatal_no_pos "elpi: failure"
+      | NoMoreSteps -> assert false
+    end;
+    t, ty
+
+let lpq : Quotation.quotation = fun ~depth st _loc text ->
+  let open Parsing in
+  let ast = Parser.Lp.parse_string "xxx" ("type " ^ text ^ ";") in
+  match ast |> Stream.next |> fun x -> x.Common.Pos.elt with
+  | Syntax.P_query { Common.Pos.elt = Syntax.P_query_infer(t,_); _ } ->
+      (*Printf.eprintf "Q %s\n" text;*)
+      let t, pats = !scope_ref t in
+      let st, t, _ = embed_term ~pats ~depth st t in
+      st, t
+  | _ -> assert false
+
+let () = Quotation.set_default_quotation lpq
diff --git a/src/handle/query.ml b/src/handle/query.ml
index e12b4c5d0..5c94e11de 100644
--- a/src/handle/query.ml
+++ b/src/handle/query.ml
@@ -7,15 +7,20 @@ open Proof
 open Lplib open Base
 open Timed
 
-let infer : Pos.popt -> problem -> ctxt -> term -> term * term =
-  fun pos p ctx t ->
+let infer : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list) -> Sig_state.t -> Pos.popt -> problem -> ctxt -> term -> term * term =
+  fun ?scope ss pos p ctx t ->
   match Infer.infer_noexn p ctx t with
   | None -> fatal pos "%a is not typable." term t
   | Some (t, a) ->
       if Unif.solve_noexn p then
         begin
-          if !p.unsolved = [] then (t, a)
-          else
+          if !p.unsolved = [] then begin
+            let t, a = Elpi_handle.solve_tc ?scope ss pos p ctx (t, a) in
+            match Infer.infer_noexn p ctx t with
+            | None -> fatal pos "%a is not typable AFTER TC RESOLUTION!!!!" term t
+            | _ -> Common.Console.out 1 "TC RESOLUTION OK!@ ";
+               t, a
+          end else
             (List.iter (wrn pos "Cannot solve %a." constr) !p.unsolved;
              fatal pos "Failed to infer the type of %a." term t)
         end
@@ -179,9 +184,9 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
       Console.out 2 "assertion: it is %b that %a" (not must_fail)
         constr (ctxt, t, u);
       (* Check that [t] is typable. *)
-      let (t, a) = infer pt.pos p ctxt t in
+      let (t, a) = infer ss pt.pos p ctxt t in
       (* Check that [u] is typable. *)
-      let (u, b) = infer pu.pos p ctxt u in
+      let (u, b) = infer ss pu.pos p ctxt u in
       (* Check that [t] and [u] have the same type. *)
       p := {!p with to_solve = (ctxt,a,b)::!p.to_solve};
       if Unif.solve_noexn p then
@@ -200,8 +205,12 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
       None
   | P_query_infer(pt, cfg) ->
       let t = scope pt in
-      return term (Eval.eval cfg ctxt (snd (infer pt.pos p ctxt t)))
+      let scope = Scope.scope_term_w_pats ~typ:false ~mok true ss env in
+      let t, ty = infer ss ~scope pt.pos p ctxt t in
+      let t = Eval.eval cfg ctxt t in
+      let ty = Eval.eval cfg ctxt ty in
+      return typing (ctxt,t,ty)
   | P_query_normalize(pt, cfg) ->
       let t = scope pt in
-      let t, _ = infer pt.pos p ctxt t in
+      let t, _ = infer ss pt.pos p ctxt t in
       return term (Eval.eval cfg ctxt t)
diff --git a/src/handle/query.mli b/src/handle/query.mli
index 83eadb07f..23db36608 100644
--- a/src/handle/query.mli
+++ b/src/handle/query.mli
@@ -10,7 +10,7 @@ open Proof
     refinement of [t]. Note that [p] gets modified. Context [c] must well
     sorted.
     @raise Fatal if [t] cannot be typed. *)
-val infer : popt -> problem -> ctxt -> term -> term * term
+val infer : ?scope:(Parsing.Syntax.p_term -> Core.Term.term * (int * string) list) -> Sig_state.t -> popt -> problem -> ctxt -> term -> term * term
 
 (** [check pos p c t a] checks that the term [t] has type [a] in context [c]
     and under the constraints of [p], and returns [t] refined. Context [c]
diff --git a/src/handle/rewrite.ml b/src/handle/rewrite.ml
index ffd8f8c02..4ae6aa60c 100644
--- a/src/handle/rewrite.ml
+++ b/src/handle/rewrite.ml
@@ -321,7 +321,7 @@ let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool ->
 
   (* Infer the type of [t] (the argument given to the tactic). *)
   let g_ctxt = Env.to_ctxt g_env in
-  let (t, t_type) = Query.infer pos p g_ctxt t in
+  let (t, t_type) = Query.infer ss pos p g_ctxt t in
 
   (* Check that [t_type ≡ Π x1:a1, ..., Π xn:an, P (eq a l r)]. *)
   let (a, l, r), vars  = get_eq_data cfg pos t_type in
diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
index 3fdd7bea1..c0dbf3745 100644
--- a/src/handle/tactic.ml
+++ b/src/handle/tactic.ml
@@ -41,7 +41,7 @@ let add_axiom : Sig_state.t -> popt -> meta -> sym =
     (* We ignore the new ss returned by Sig_state.add_symbol: axioms do not
        need to be in scope. *)
     snd (Sig_state.add_symbol ss
-           Public Defin Eager true id !(m.meta_type) [] None)
+           Public Defin Eager true id !(m.meta_type) [] false false None)
   in
   (* Create the value which will be substituted for the metavariable. This
      value is [sym x0 ... xn] where [xi] are variables that will be
diff --git a/src/parsing/dkLexer.mll b/src/parsing/dkLexer.mll
index a64dcaf29..170667e92 100644
--- a/src/parsing/dkLexer.mll
+++ b/src/parsing/dkLexer.mll
@@ -53,6 +53,8 @@ rule token = parse
   | "#ASSERTNOT"{ ASSERTNOT  ( get_loc lexbuf ) }
   | "#PRINT"    { PRINT      ( get_loc lexbuf ) }
   | "#GDT"      { GDT        ( get_loc lexbuf ) }
+  | "#TYPE_CLASS" space+ (ident as md)     { TYPE_CLASS        ( get_loc lexbuf , mk_ident md) }
+  | "#TYPE_CLASS_INSTANCE"  space+ (ident as md)    { TYPE_CLASS_INSTANCE        ( get_loc lexbuf , mk_ident md) }
   | mident as md '.' (ident as id)
   { QID ( get_loc lexbuf , mk_mident md , mk_ident id ) }
   | ident  as id
diff --git a/src/parsing/dkParser.mly b/src/parsing/dkParser.mly
index 9f70d0f45..26d74dfb0 100644
--- a/src/parsing/dkParser.mly
+++ b/src/parsing/dkParser.mly
@@ -79,6 +79,9 @@
 
     let require (lps,id) = make_pos lps (P_require(false,[make_pos lps [id]]))
 
+    let type_class (lps,id) = make_pos lps (P_type_class (make_pos lps id))
+    let type_class_instance (lps,id) = make_pos lps (P_type_class_instance (make_pos lps id))
+
 %}
 
 %token EOF
@@ -107,6 +110,8 @@
 %token <DkTokens.loc> UNDERSCORE
 %token <DkTokens.loc*DkBasic.mident> NAME
 %token <DkTokens.loc*DkBasic.mident> REQUIRE
+%token <DkTokens.loc*DkBasic.mident> TYPE_CLASS
+%token <DkTokens.loc*DkBasic.mident> TYPE_CLASS_INSTANCE
 %token <DkTokens.loc> TYPE
 %token <DkTokens.loc> KW_DEF
 %token <DkTokens.loc> KW_DEFAC
@@ -199,6 +204,8 @@ line:
   | GDT   QID    DOT { fail $1 "Unsupported command" }
   | n=NAME       DOT { fail (fst n) "Unsupported command" }
   | r=REQUIRE    DOT { require r }
+  | tc=TYPE_CLASS DOT { type_class tc }
+  | tci=TYPE_CLASS_INSTANCE DOT { type_class_instance tci }
   | EOF              {raise End_of_file}
 
 eval_config:
diff --git a/src/parsing/dkTokens.ml b/src/parsing/dkTokens.ml
index 90b1aa4b7..fb1a8b87a 100644
--- a/src/parsing/dkTokens.ml
+++ b/src/parsing/dkTokens.ml
@@ -19,6 +19,8 @@ type token =
   | QID of (loc * mident * ident)
   | NAME of (loc * mident)
   | REQUIRE of (loc * mident)
+  | TYPE_CLASS of (loc * ident)
+  | TYPE_CLASS_INSTANCE of (loc * ident)
   | LONGARROW
   | LEFTSQU
   | LEFTPAR
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index ff575c8c2..34c6ee188 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -45,7 +45,9 @@ type token =
   | COMPUTE
   | CONSTANT
   | DEBUG
+  | ELPI
   | END
+  | EXISTING
   | FAIL
   | FLAG
   | GENERALIZE
@@ -55,6 +57,7 @@ type token =
   | INDUCTIVE
   | INFIX
   | INJECTIVE
+  | INSTANCE
   | LET
   | NOTATION
   | OPAQUE
@@ -80,6 +83,7 @@ type token =
   | SYMMETRY
   | TYPE_QUERY
   | TYPE_TERM
+  | TYPECLASS
   | UNIF_RULE
   | VERBOSE
   | WHY3
@@ -208,7 +212,9 @@ let rec token lb =
   | "compute" -> COMPUTE
   | "constant" -> CONSTANT
   | "debug" -> DEBUG
+  | "elpi" -> ELPI
   | "end" -> END
+  | "existing" -> EXISTING
   | "fail" -> FAIL
   | "flag" -> FLAG
   | "generalize" -> GENERALIZE
@@ -218,6 +224,7 @@ let rec token lb =
   | "inductive" -> INDUCTIVE
   | "infix" -> INFIX
   | "injective" -> INJECTIVE
+  | "instance" -> INSTANCE
   | "left" -> SIDE(Pratter.Left)
   | "let" -> LET
   | "notation" -> NOTATION
@@ -246,6 +253,7 @@ let rec token lb =
   | "symbol" -> SYMBOL
   | "symmetry" -> SYMMETRY
   | "type" -> TYPE_QUERY
+  | "typeclass" -> TYPECLASS
   | "TYPE" -> TYPE_TERM
   | "unif_rule" -> UNIF_RULE
   | "verbose" -> VERBOSE
diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
index 8c24556b8..b1d106cd6 100644
--- a/src/parsing/lpParser.mly
+++ b/src/parsing/lpParser.mly
@@ -38,7 +38,9 @@
 %token COMPUTE
 %token CONSTANT
 %token DEBUG
+%token ELPI
 %token END
+%token EXISTING
 %token FAIL
 %token FLAG
 %token GENERALIZE
@@ -48,6 +50,7 @@
 %token INDUCTIVE
 %token INFIX
 %token INJECTIVE
+%token INSTANCE
 %token LET
 %token NOTATION
 %token OPAQUE
@@ -73,6 +76,7 @@
 %token SYMMETRY
 %token TYPE_QUERY
 %token TYPE_TERM
+%token TYPECLASS
 %token UNIF_RULE
 %token VERBOSE
 %token WHY3
@@ -136,8 +140,12 @@ command:
     { make_pos $sloc (P_require(false,l)) }
   | REQUIRE p=path AS i=uid SEMICOLON
     { make_pos $sloc (P_require_as(p,i)) }
-  | OPEN l=list(path) SEMICOLON
-    { make_pos $sloc (P_open l) }
+  | OPEN f=list(STRINGLIT) l=list(path) SEMICOLON
+    { make_pos $sloc (P_open(f,l)) }
+  | EXISTING INSTANCE id=UID SEMICOLON
+    { make_pos $sloc (P_type_class_instance(make_pos $sloc id)) }
+  | EXISTING TYPECLASS id=UID SEMICOLON
+    { make_pos $sloc (P_type_class(make_pos $sloc id)) }
   | ms=modifier* SYMBOL s=uid_or_nat al=param_list* COLON a=term
     po=proof? SEMICOLON
     { let sym =
@@ -162,6 +170,8 @@ command:
   | NOTATION i=qid_or_nat n=notation SEMICOLON
     { make_pos $loc (P_notation(i,n)) }
   | q=query SEMICOLON { make_pos $sloc (P_query(q)) }
+  | ELPI f=STRINGLIT p=STRINGLIT a=term SEMICOLON
+    { make_pos $sloc (P_elpi(f,p,a)) }
   | EOF { raise End_of_file }
 
 query:
@@ -202,6 +212,8 @@ modifier:
   | PRIVATE { make_pos $sloc (P_expo Term.Privat) }
   | PROTECTED { make_pos $sloc (P_expo Term.Protec) }
   | SEQUENTIAL { make_pos $sloc (P_mstrat Term.Sequen) }
+  | TYPECLASS { make_pos $sloc P_typeclass }
+  | INSTANCE { make_pos $sloc P_typeclass_instance }
 
 uid: s=UID { make_pos $sloc s}
 
diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml
index 2a7da85ee..c382478b9 100644
--- a/src/parsing/parser.ml
+++ b/src/parsing/parser.ml
@@ -85,7 +85,7 @@ module Dk : PARSER = struct
 
   let command :
     (Lexing.lexbuf -> DkTokens.token) -> Lexing.lexbuf -> Syntax.p_command =
-    let r = ref (Pos.none (Syntax.P_open [])) in fun token lb ->
+    let r = ref (Pos.none (Syntax.P_open([],[]))) in fun token lb ->
     Debug.(record_time Parsing (fun () -> r := DkParser.line token lb)); !r
 
   let stream_of_lexbuf :
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index 25a8894af..ae26d25b9 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -314,7 +314,9 @@ let command : p_command pp = fun ppf { elt; _ } ->
       (inductive "inductive") i (List.pp with_ind "") il
   | P_notation (qid, n) ->
     out ppf "notation %a %a" qident qid (Print.notation string) n
-  | P_open ps -> out ppf "open %a" (List.pp path " ") ps
+  | P_open(f,ps) -> out ppf "open %a %a"
+      (List.pp (fun fmt x ->
+         Format.fprintf fmt "\"%s\"" x) "") f (List.pp path " ") ps
   | P_query q -> query ppf q
   | P_require (b, ps) ->
     out ppf "require%a %a" (pp_if b (unit " open")) () (List.pp path " ") ps
@@ -338,6 +340,9 @@ let command : p_command pp = fun ppf { elt; _ } ->
     end
   | P_unif_rule ur -> out ppf "unif_rule %a" unif_rule ur
   | P_coercion c -> out ppf "%a" (rule "coerce_rule") c
+  | P_elpi _ -> assert false
+  | P_type_class ({Pos.elt = id}) -> out ppf "existing typeclass %s" id
+  | P_type_class_instance ({Pos.elt = id}) -> out ppf "existing instance %s" id
   end;
   out ppf ";"
 
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index 964e18d1d..525d05e0a 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -483,12 +483,28 @@ let scope =
     a type (defaults to [false]). No {b new} metavariables may appear in
     [t], but metavariables in the image of [mok] may be used. The function
     [mok] defaults to the function constant to [None] *)
-let scope_term : ?typ:bool -> ?mok:(int -> meta option) ->
+let scope_term: ?typ:bool -> ?mok:(int -> meta option) ->
   bool -> sig_state -> env -> p_term -> term =
   fun ?(typ=false) ?(mok=fun _ -> None) m_term_prv ss env t ->
   let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in
   Bindlib.unbox (scope ~typ 0 md ss env t)
 
+let scope_term_w_pats: ?typ:bool -> ?mok:(int -> meta option) ->
+  bool -> sig_state -> env -> p_term -> term * (int * string) list =
+  fun ?(typ=false) ?(mok=fun _ -> None) m_term_prv ss env t ->
+    let names = Hashtbl.create 1 in
+    let md = M_LHS {
+      m_lhs_prv = false;
+      m_lhs_indices = Hashtbl.create 1;
+      m_lhs_arities = Hashtbl.create 1;
+      m_lhs_names = names;
+      m_lhs_size = 0;
+      m_lhs_in_env = []
+    } in
+    let t = Bindlib.unbox (scope ~typ 0 md ss env t) in
+    t, List.of_seq (Hashtbl.to_seq names)
+  
+
 (** [patt_vars t] returns a couple [(pvs,nl)]. The first compoment [pvs] is an
     association list giving the arity of all the “pattern variables” appearing
     in the parser-level term [t]. The second component [nl] contains the names
diff --git a/src/parsing/scope.mli b/src/parsing/scope.mli
index 91d2cb6c8..5478c442f 100644
--- a/src/parsing/scope.mli
+++ b/src/parsing/scope.mli
@@ -18,6 +18,11 @@ val scope_term :
   ?mok:(int -> meta option) ->
   bool -> sig_state -> env -> p_term -> term
 
+val scope_term_w_pats :
+  ?typ:bool (* default: false *) ->
+  ?mok:(int -> meta option) ->
+  bool -> sig_state -> env -> p_term -> term * (int * string) list
+
 (** Representation of a rewriting rule prior to SR-checking. *)
 type pre_rule =
   { pr_sym      : sym
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index 7780c76c4..38431d55c 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -234,6 +234,8 @@ type p_modifier_aux =
   | P_expo of Term.expo (** visibility of symbol outside its modules *)
   | P_prop of Term.prop (** symbol properties: constant, definable, ... *)
   | P_opaq (** opacity *)
+  | P_typeclass
+  | P_typeclass_instance
 
 type p_modifier = p_modifier_aux loc
 
@@ -257,7 +259,9 @@ type p_command_aux =
   | P_require  of bool * p_path list
     (* "require open" if the boolean is true *)
   | P_require_as of p_path * p_ident
-  | P_open of p_path list
+  | P_type_class of p_ident
+  | P_type_class_instance of p_ident
+  | P_open of string list * p_path list
   | P_symbol of p_symbol
   | P_rules of p_rule list
   | P_inductive of p_modifier list * p_params list * p_inductive list
@@ -266,6 +270,7 @@ type p_command_aux =
   | P_unif_rule of p_rule
   | P_coercion of p_rule
   | P_query of p_query
+  | P_elpi of string * string * p_term
 
 (** Parser-level representation of a single (located) command. *)
 type p_command = p_command_aux loc
@@ -408,7 +413,7 @@ let eq_p_command : p_command eq = fun {elt=c1;_} {elt=c2;_} ->
   match c1, c2 with
   | P_require(b1,l1), P_require(b2,l2) ->
       b1 = b2 && List.eq eq_p_path l1 l2
-  | P_open l1, P_open l2 -> List.eq eq_p_path l1 l2
+  | P_open(f1,l1), P_open (f2,l2) -> List.eq Stdlib.String.equal f1 f2 && List.eq eq_p_path l1 l2
   | P_require_as(m1,i1), P_require_as(m2,i2) ->
       eq_p_path m1 m2 && eq_p_ident i1 i2
   | P_symbol s1, P_symbol s2 -> eq_p_symbol s1 s2
diff --git a/tcsolver.elpi b/tcsolver.elpi
new file mode 100644
index 000000000..74f561046
--- /dev/null
+++ b/tcsolver.elpi
@@ -0,0 +1,63 @@
+msolve L :- 
+  print "### GOALS: " L,
+  compile_all Cl,
+  print "RULES:" Cl,
+  Cl => std.forall L (open tc).
+
+pred open i:(symbol -> term -> term -> prop), i:sealed-goal.
+open P (nabla F) :- pi x\ open P (F x).
+open P (seal (goal Ctx Ty Wit)) :- var Wit,
+  print "TC PROBLEM:\n" Ctx "|-\n" Wit ":" Ty "\n",
+  Ty = appl (appl {{ bios.Term }} _) Term,
+  print "PROCEED" Term,
+  safe-dest-app Term (symb Class) _,
+  not (var Class),
+  lp.tc? Class, !,
+  Ctx => P Class Ty Wit,
+  print "TC INSTANCE:\n" Ctx "|-\n" Wit ":" Ty "\n".
+open P (seal (goal Ctx Ty Wit)) :-
+  print "NOT A TC INFERENCE PROBLEM:\n" Ctx "|-\n" Wit ":" Ty "\n".
+
+pred tc o:symbol, o:term, o:term.
+
+pred safe-dest-app i:term, o:term, o:list term.
+safe-dest-app (appl HD ARG) H AS :- !,
+  safe-dest-app HD H A,
+  std.append A [ARG] AS.
+safe-dest-app X X [].
+
+pred compile i:term, i:list prop, i:term, o:prop.
+compile (prod (appl (appl {{ bios.Term }} _Univ) Term as W) F) TODO H (pi x\ C x) :-
+  safe-dest-app Term (symb S) _, lp.tc? S,
+  !,
+  pi x\
+    compile (F x) [tc S W x |TODO] (appl H x) (C x).
+
+compile (prod (appl T U) F) TODO H (pi x\ C x) :-
+  T = symb S, lp.tc? S,
+  !,
+  pi x\
+    compile (F x) [tc S (appl T U) x |TODO] (appl H x) (C x).
+
+compile (prod _ F) TODO H (pi x\ C x) :-
+  !,
+  pi x\
+    compile (F x) TODO (appl H x) (C x).
+
+compile (appl (appl {{ bios.Term }} Univ) Term) TODO HD (pi u t\ tc S (End u t) HD :- [Conv u t|TODO]) :- !,
+  safe-dest-app Term (symb S) _,
+  pi u t\
+    End u t = (appl (appl {{ bios.Term }} u) t),
+    Conv u t = (/*lp.eq_modulo*/ u = Univ, (t = Term ; (sigma T'\ sigma Term'\ lp.snf t T', lp.snf Term Term', (T' = Term')) ; lp.eq_modulo t Term)).
+    /*Conv u t = (/*lp.eq_modulo*/ u = Univ, std.spy(lp.unif t Term)). */
+  
+
+compile End TODO HD (tc S End HD :- TODO) :- safe-dest-app End (symb S) _. 
+
+pred compile_all o:list prop.
+compile_all Props :-
+  lp.tc-instances Candidates,
+  print "instances" Candidates,
+  std.map Candidates
+    (N\claus\ sigma T\ lp.sig N T, compile T [] (symb N) claus)
+    Props.
diff --git a/tests/OK/elpitest.elpi b/tests/OK/elpitest.elpi
new file mode 100644
index 000000000..748347590
--- /dev/null
+++ b/tests/OK/elpitest.elpi
@@ -0,0 +1,29 @@
+main T T1 :-
+  print "before type inference" T,
+  of T _,
+  print "\nafter type inference" T,
+  T1 = T.
+
+
+pred of i:term, o:term.
+
+% API to access the type of a symbol
+of (symb S) T :- lp.sig S T.
+
+% silly rules
+of (prod A B) T :-
+  of A typ,
+  pi x\ of x A => of (B x) T.
+
+of (appl H A) Ta :-
+  of H (prod S T),
+  of A S,
+  Ta = T A.
+
+% suspension of typing on holes (type constraint)
+of U T :- var U, declare_constraint (of U T) [U].
+
+% uniqueness of typing
+constraint of {
+  rule (of (uvar X _) T) \ (of (uvar X _) S) <=> (S = T).
+}
diff --git a/tests/OK/elpitest.lp b/tests/OK/elpitest.lp
new file mode 100644
index 000000000..5c38d5fa1
--- /dev/null
+++ b/tests/OK/elpitest.lp
@@ -0,0 +1,45 @@
+/* dune exec lambdapi check tests/OK/elpitest.lp */
+require open tests.OK.logic;
+require open tests.OK.bool;
+require open tests.OK.nat;
+
+flag "print_implicits" on; // default is off
+flag "print_contexts" on; // default is off
+flag "print_domains" on; // default is off
+flag "print_meta_types" on; // default is off
+
+constant typeclass symbol eqdec : U → TYPE;
+constant symbol mk_eqdec [i] :
+  Π (f : T i → T i → B),
+  // (Π (x y : T i), P ({|and|} (imp (x = y) (f x y = true))(imp (f x y = true) (x = y))))  →
+  eqdec i;
+
+symbol == [i:U] [j:eqdec i] : T i → T i → B;
+notation == infix 1;
+
+/* extra stdlib */
+symbol eq_bool : B → B → B ≔ λ b1 b2, bool_neg (bool_xor b1 b2);
+symbol Pair : U → U → TYPE;
+symbol mk_Pair [i] [j] : T i → T j → Pair i j;
+symbol pair : U → U → U;
+rule T (pair $i $j) ↪ Pair $i $j;
+
+symbol bool_eqdec : eqdec bool ≔ mk_eqdec eq_bool /* p */;
+existing instance bool_eqdec;
+instance symbol nat_eqdec  : eqdec nat ≔ mk_eqdec eq_nat /* p */;
+instance symbol pair_eqdec : Π i j, eqdec i → eqdec j → eqdec (pair i j);
+  /* ≔ mk_eqdec eq_nat ; */
+
+type λ b , true == b;
+type λ n , 1 == n;
+type λ n : T nat, λ b : T bool, mk_Pair 1 true == mk_Pair n b;
+
+rule @== _ (@mk_eqdec _ $f /* _ */) ↪ $f;
+
+compute true == true;
+compute true == false;
+compute 1 == 0;
+
+// assert ⊢ eqop _ true false : B;
+// elpi "tests/OK/elpitest.elpi" "main"
+//  (Π x y , P (x = y) → P (y = x));
diff --git a/tests/rewriting.ml b/tests/rewriting.ml
index 4a945c469..ec8609bed 100644
--- a/tests/rewriting.ml
+++ b/tests/rewriting.ml
@@ -15,7 +15,7 @@ let scope_term ss = Scope.scope_term true ss []
 
 let add_sym ss id =
   Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Kind []
-    None
+    false false None
 
 (* Define a signature state and some symbols. *)