Maplet Overriding in Goal
This page describes the design of a tactic requested here : Feature Request #3306228
Split every goal in the form : into two sub-goals if and only if the sequent contains a hypothesis such as :
Where denote either a Relation , or a Total Relation , or a Partial Function , or a Total Function , and is such as .
Those two subgoals and the predicate are not equivalent to the goal. Indeed, in the case is a Relation, the goal is equivalent to . But this has the drawback of writing three times the expression x. If this expression is big, then it can make the proof rule hard to read.
But, we know that for all the relation given in Objective. By ensuring that is among the hypotheses of the sequent, we ensure that the first predicate of the conjunction is provable. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writing instead of .