On Tuesday, October 29, 2019 at 10:46:39 PM UTC+1, Norman Megill wrote: > > > In order to use a theorem with implicit substitution, the proof usually > eliminates the implicit substitution hypotheses with a chain of equality > and/or biconditional theorems. The hypotheses are then completely > eliminated, and ph is hardly ever needed to achieve that (if ever). So we > rarely bother to add a ph antecedent. Offhand I can't recall a case where > it would have helped in practice. > > > Although the cases may be rare, they do exist (as Olivier`s case shows, and I had such cases, too - unfortunately, I do not exactly remember them). And it takes always a long time to find a proper solution. On the other way round, if we had an antecedent ( ph /\ ... ) in a hypothesis and we do not need it, it is a matter of about one second to apply ~ adantl to remove the ph and to continue. Therefore, it should be a recommendation (not an obligation) to provide such hypotheses ( $e |- ( ( ph /\ x = Y ) -> A = B ) $. ) instead of $e |- ( x = Y -> A = B ) $. , as I proposed in my yesterdays post. As Olivier correctly stated, $e |- ( x = Y -> A = B ) $. is "stronger", i.e. more restrictive than $e |- ( ( ph /\ x = Y ) -> A = B ) $. - and I think we should preferably provide theorems with the weakest assumptions as possible.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/24d15625-52c1-42fb-842d-9e0cbcd31801%40googlegroups.com.
