proposition: Lemma sig_eq {A} (P : A -> Prop) : forall (mx my : sig P), proj1_sig mx = proj1_sig my -> mx = my.
proof: Proof. intros [cx ex] [cy ey]. simpl. induction 1. have hintUnif : ex = ey. by apply ax_proof_irrel. rewrite hintUnif. reflexivity. Defined.
imports: Mon(Base) mathcomp(ssreflect)