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
reduced *)
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
reduced *)