proposition: Lemma sig_eq : forall x y : sig P, proj1_sig x = proj1_sig y <-> x = y.
proof: Proof. intros [x_val x] [y_val y]; simpl. split; intro e. subst y_val. rewrite (proof_irrelevance _ x y). refl. gen (f_equal (@proj1_sig _ _) e). tauto. Qed.
imports: CoLoR(LogicUtil) CoLoR(FunUtil)