proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings