(* ITERATED ABSTRACTION *****************************************************)
definition labst: nat → lterm → lterm ≝ λh,M. match M with
(* ITERATED ABSTRACTION *****************************************************)
definition labst: nat → lterm → lterm ≝ λh,M. match M with