Definition weqdnicoprod_compute {n : nat} (j : ⟦S n⟧ ) : weqdnicoprod_provisional n j ~ weqdnicoprod_map j. Proof. intros. intros i. induction i as [i|i]. - apply subtypePath_prop. induction i as [i I]. apply idpath. - apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.