let decurry = List.length classes - List.length tl in
if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
let decurry = List.length classes - List.length tl in
if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
match rc with
| Some (i, j) when i > 1 && i <= List.length classes ->
let classes, tl, _, what = split2_last classes tl in
let script, what = mk_atomic st dtext what in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
match rc with
| Some (i, j) when i > 1 && i <= List.length classes ->
let classes, tl, _, what = split2_last classes tl in
let script, what = mk_atomic st dtext what in
let qs = mk_bkd_proofs (next st) synth classes tl in
if is_rewrite_right hd then
List.rev script @ convert st t @
let qs = mk_bkd_proofs (next st) synth classes tl in
if is_rewrite_right hd then
List.rev script @ convert st t @
Some [T.Apply (v, dtext ^ "dependent")]
in
T.list_map2_filter aux classes ts
Some [T.Apply (v, dtext ^ "dependent")]
in
T.list_map2_filter aux classes ts