NCic.context -> NCic.term ->
NCic.term
-val are_convertible :
- ?subst:NCic.substitution ->
- NCic.context -> NCic.term -> NCic.term ->
- bool
+val are_convertible :
+ ?subst:NCic.substitution ->
+ (subst:NCic.substitution ->
+ NCic.context -> NCic.term -> bool list) ->
+ NCic.context -> NCic.term -> NCic.term -> bool
+
(* performs head beta/(delta)/cast reduction; the default is to not perform
delta reduction; if provided, ~upto is the maximum number of beta redexes