proposition: Lemma isdeceqtoisapartdec ( X : hSet ) ( is : isdeceq X ) : isapartdec ( tpair _ ( deceqtoneqapart is ) ).
proof: Proof. intros a b. destruct ( is a b ) as [ l | r ]. - apply ii2. assumption. - apply ii1. intros f. apply r. assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids