You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Now ANG still use Fact, not PtNe.
We should change every theorem with conditions of \ne into [PtNe ] and conclusions of \ne into [PtNe] too.
not all theorems should be written as instance.
but it provide a good form for future tactics