-(* CSC: old code that never performs beta reduction
- let appl_fun um_aux he tl =
- let tl' = List.map um_aux tl in
- begin
- match um_aux he with
- Cic.Appl l -> Cic.Appl (l@tl')
- | he' -> Cic.Appl (he'::tl')
- end
- in
- apply_subst_gen ~appl_fun
-*)