match li with
C.AConst (sid,uri,exp_named_subst)::args ->
if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or
- UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI then
+ UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI or
+ LibraryObjects.is_eq_ind_URI uri or
+ LibraryObjects.is_eq_ind_r_URI uri then
let subproofs,arg =
(match
build_subproofs_and_args