Open jjdishere opened 6 months ago
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
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