Argument for using_well_founded
rel_tac has to synthesize an element of type (has_well_founded A).
The two arguments are: a local representing the function being defined by well
founded recursion, and a list of recursive equations.
The equations can be used to decide which well founded relation should be used.
dec_tac has to synthesize decreasing proofs.