(* *)
(**************************************************************************)
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
(* DEGREE ASSIGNMENT **********************************************************)
(* The degree of a term *******************************************************)
>append_Deg >append_Deg <Hvw -Hvw >DegHd_Lift; [2: //]
>deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/
qed.
+*)