Context-extension for dependent-types (unif_rule BUG?)

[1337777]

This file will compare a usual traditional context-extension
(categories with families, etc) versus a more general and clearer
direct computational (strictified via Lambdapi rewrite rules) implementation
as required for a proof assistant for categories/sheaves/schemes

[1337777]

This pull requests also exposes a potential bug in Lambdapi unif_rule ? The minimal example scenario is simple:

for any injective symbol Context_cat and for a rule (Context_cat (Terminal_catd $A)) ↪ $A then the following attempt to temporarily bypass injectivity does not work and Lambdapi raises an error when trying to register the rule, but it should work?

//ERROR:
unif_rule Context_cat $B ≡ (Context_cat (Terminal_catd (Context_cat $X))) ↪ [ $B ≡ $X];

[fblanqui]

Hi. Could you please open an issue with a minimal example of what you would like to do and why?