| NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
| NCic.Appl [] -> assert false
| NCic.Appl l when depth > 10 || List.length l > 50 -> [Variable]
| NCic.Appl (hd::tl) ->
aux (List.length tl) depth hd @
List.flatten (List.map (aux 0 (depth+1)) tl)
| NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
| NCic.Appl [] -> assert false
| NCic.Appl l when depth > 10 || List.length l > 50 -> [Variable]
| NCic.Appl (hd::tl) ->
aux (List.length tl) depth hd @
List.flatten (List.map (aux 0 (depth+1)) tl)