Lemma stn_eq_or_neq_symm_nondep {n} {x y : ⟦n⟧%stn} (de_xy : (x = y) ⨿ (x ≠ y)%stn) (de_yx : (y = x) ⨿ (y ≠ x)%stn) {Z} (z1 z2 : Z) : coprod_rect (fun _ => Z) (fun _ => z1) (fun _ => z2) de_xy = coprod_rect (fun _ => Z) (fun _ => z1) (fun _ => z2) de_yx. Proof. destruct de_xy as [e_xy | ne_xy]; destruct de_yx as [e_yx | ne_yx]; simpl; try reflexivity; eapply fromempty, nat_neq_to_nopath; try eassumption; apply pathsinv0, maponpaths; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.