We use an implication from the subgoals to the goal
rather than the implication of the conjunction of the subgoals

Fixes declaration "^" of theory "exponentation"

This reverts commit 9585eda5.

nth projections rewrite to car and cdr.
theory "real_defs" wouldn't typecheck because (nth 1 x) would not reduce
when x is a variable, and thus no subtyping could be performed (subtyping
uses car and cdr

Unified documentation in README
Removed unused encodings
Removed sandbox
Removed psnj
More documentation in encoding and in test.lisp

that may actually fail

Collect them directly from the theory of the (current) context

Look into the resolution to know whether a name is a bound variable

formal theory parameters are registered as such and printed as bindings,
the constant +type+ is not used anymore

and better handling of implicitness

Updated test looks fishy

Coercions on dependent tuples as well as from non dependent tuples to
dependent tuples

To avoid leaving altered global variables when pp-dk finishes

Update to lambdapi 2 (which uses a new coercion insertion algorithm)

New typechecker requires more resources in some cases