+let classify_conclusion vs =
+ let rec get_argsno = function
+ | c, C.Appl (t :: vs) ->
+ let hd, argsno = get_argsno (c, t) in
+ hd, argsno + List.length vs
+ | _, t -> t, 0
+ in
+ let inside i = i > 1 && i <= List.length vs in
+ match vs with
+ | v0 :: v1 :: _ ->
+ let hd0, a0 = get_argsno v0 in
+ let hd1, a1 = get_argsno v1 in
+ begin match hd0, hd1 with
+ | C.Rel i, C.MutInd (u, n, _) when inside i -> Some (i, a0, u, n)
+ | _ -> None
+ end
+ | _ -> None
+