+ | C.AAppl (_, hd :: tl) ->
+ let ty = match get_inner_types st hd with
+ | Some (ity, _) -> H.cic ity
+ | None -> get_type "TC3" st hd
+ in
+ let classes, _ = Cl.classify st.context ty in
+ let parsno, argsno = List.length classes, List.length tl in
+ let decurry = parsno - argsno in
+ if decurry <> 0 then begin
+(* FG: we fall back in the cut case *)
+ assert (Ut.is_sober st.context (H.cic ety));
+ let ety = H.acic_bc st.context ety in
+ let qs = [proc_proof (next st) v; [T.Id ""]] in
+ st, [T.Branch (qs, ""); T.Cut (intro, ety, dtext)]
+ end else
+ let names, synth = get_sub_names hd tl, I.S.empty in
+ let qs = proc_bkd_proofs (next st) synth names classes tl in
+ let hd = mk_lapply_args hd tl classes in
+ let qs = [T.Id ""] :: qs in
+ st, [T.Branch (qs, ""); T.LApply (intro, hd, dtext)]