[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Identical antecedent and consequent


Try doing Meta-x show-expanded-sequent on the goal.  This command
expands the names of the various function symbols in the sequent.
This may reveal some reasons (overloading, etc.) why the two
(potentially equivalent) seemingly identical formulas are different.
That can give you further clue about completing the proof.

- Srivas