Definition weqfromcoprodofstn_map (n m : nat) : (⟦n⟧ ⨿ ⟦m⟧) -> ⟦n+m⟧. Proof. intros i. induction i as [i | i]. - apply stn_left. assumption. - apply stn_right. assumption. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.