proposition: Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)} (x y : sig P) : x = y ↔ `x = `y.
proof: Proof. split; [intros <-; reflexivity|]. destruct x as [x Hx], y as [y Hy]; simpl; intros; subst. f_equal. apply proof_irrel. Qed.
imports: stdpp(options)