If there is an hypothesis P(x) and a goal P(y), a tactic could generate a proof obligation for x=y. It would be easier and less error-prone than using ah with a handwritten equality.
This is quite difficult to implement. We would need to have a unification algorithm on predicates.
Log in to post a comment.
This is quite difficult to implement. We would need to have a unification algorithm on predicates.