+let rec no_leading_lambdas hd_var j = function\r
+ | L t -> 1 + no_leading_lambdas (hd_var+1) j t\r
+ | A _ as t -> let hd_var', n = get_inert t in if hd_var = hd_var' then max 0 (j - n) else 0\r
+ | V n -> if n = hd_var then j else 0\r
+ | B | C _ -> 0\r
+;;\r