meta def tactic.mk_brec_on_rec_value (F_name : name) (i : ℕ) :
Construct brec_on "recursive value". F_name is the name of the brec_on "dictionary". Type of the F_name hypothesis should be of the form (below (C ...)) where C is a constructor. The result is the "recursive value" for the (i+1)-th recursive value of the constructor C.
meta def tactic.constructor_num_fields (c : name) :