proposition: Lemma invmaponpathsS (n m : nat) : S n = S m -> n = m.
proof: Proof. intros e. set (f := λ n : nat, match n with O => O | S m => m end). apply (@maponpaths _ _ f (S n) (S m) e). Defined.
imports: UniMath.Foundations.Sets