- let ts, _ = Cl.split c t in
- is_appl true (List.hd ts)
+ let classes, rc = Cl.classify c t in
+ let premises, _ = PEH.split_with_whd (c, t) in
+ match rc with
+ | Some (i, j, _, _) when i > 1 && i <= List.length classes && is_eliminator premises -> true
+ | _ ->
+ let _, conclusion = List.hd premises in
+ is_appl true conclusion