CONV_TAC : (conv -> tactic)
A ?- g =============== CONV_TAC c A ?- g'
Note that the conversion c should return a theorem whose assumptions are also among the assumptions of the goal (normally, the conversion will returns a theorem with no assumptions). CONV_TAC does not fail if this is not the case, but the resulting tactic will be invalid, so the theorem ultimately proved using this tactic will have more assumptions than those of the original goal.
|- (\x.u)v = u[v/x]