proposition: Lemma subset_eq_compat : forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> exist P x p = exist P y q.
proof: Proof. intros U P x y p q H. rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed.
imports: EqdepFacts