The consequences are the following erroneous theorems: - [pth in quote.lift_theorem](https://github.com/jack-pappas/NHol/blob/master/NHol/quot.fs#L250) - [REP_ABS_PAIR](https://github.com/jack-pappas/NHol/blob/master/NHol/pair.fs#L107) - [PAIR_EQ](https://github.com/jack-pappas/NHol/blob/master/NHol/pair.fs#L121) - [FORALL_PAIR_THM](https://github.com/jack-pappas/NHol/blob/master/NHol/pair.fs#L483) - [EXISTS_PAIR_THM](https://github.com/jack-pappas/NHol/blob/master/NHol/pair.fs#L488) - [EXISTS_UNCURRY](https://github.com/jack-pappas/NHol/blob/master/NHol/pair.fs#L533) - etc. Also the messages printed out by these tactics ("solved at...") don't seem to agree with OCaml output.
The consequences are the following erroneous theorems:
Also the messages printed out by these tactics ("solved at...") don't seem to agree with OCaml output.