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
+ | Some (i, j, _, _) when i > 1 && i <= List.length classes && is_eliminator premises -> true
| _ ->
let _, conclusion = List.hd premises in
is_appl true conclusion