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

pf = proof
  intros
  refine Refl