I'm working on Peano Axioms in Agda and I've hit a bit of a sticking point
- by Schroedinger
PA6 : ?{m n} -> m = n -> n = m
is the axiom I am trying to solve and support, I've tried using a cong (from the core library) but am having troubles with the cong constructor
PA6 = cong
gets me nowhere, I know for cong I am required to supply a refl for equality and a type, but I'm, not sure what type I'm supposed to supply. Ideas?
This is for a small assignment at University, so I'd rather someone demonstrate what I've missed rather than write the acutual answer, but I'd appreciate any degree of support.