proposition: Theorem weqtoeqstn { n n' : nat } : ⟦n⟧ ≃ ⟦n'⟧ -> n = n'.
proof: Proof. revert n'. induction n as [ | n IHn ]. - intro. destruct n' as [ | n' ]. + intros; apply idpath. + intro X. apply (fromempty (negweqstn0sn _ X)). - intro n'. destruct n' as [ | n' ]. + intro X. apply (fromempty ( negweqstnsn0 n X)). + intro X. apply maponpaths. apply IHn. apply weqcutforstn. assumption. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions