add refinement application from Fixpoint