(* *)
(**************************************************************************)
-include "Basic_2/grammar/term.ma".
+include "basic_2/grammar/term.ma".
(* LOCAL ENVIRONMENTS *******************************************************)
interpretation "abstraction (local environment)"
'DxAbst L T = (LPair L Abst T).
+
+(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)