idris-0.12.3: test/regression002/reg044.idr

exjection : S a = S b -> a = b
exjection = ?pf

pf = proof
  intros
  refine Refl