Library MetaCoq.Template.utils.MCEquality


Definition transport {A} (P : A Type) {x y : A} (e : x = y) : P x P y
  := fun ueq_rect x P u y e.

Notation "p # x" := (transport _ p x) (right associativity, at level 65).

Lemma eq_rect_transport A x P u y p
  : @eq_rect A x P u y p = transport P p u.
Proof. reflexivity. Defined.