Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use nfs1v when sufficient. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use nfs1v when sufficient. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)