idris-0.9.13: test/reg044/reg044.idr

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

pf = proof
  intros
  refine refl