include "lambda/terms/term.ma".
-(* GENERALIZED ABSTRACTION **************************************************)
+include "lambda/notation/functions/annotatedabstraction_2.ma".
+
+(* ITERATED ABSTRACTION *****************************************************)
let rec abst d M on d ≝ match d with
[ O ⇒ M