Theorem weqtoeqstn { n n' : nat } : ⟦n⟧ ≃ ⟦n'⟧ -> n = n'. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.