Rewrite equality in type definitions in Coq

Rewrite equality in type definitions in Coq.v

From Coq Require Import Init.Logic.

Axiom X: Type.
Axiom a b: X.

Axiom P: X -> Prop.
Axiom Q: P b -> Prop.

(*

  Our goal is to state an axiom like `forall (pa: P a), a = b -> Q pa`.

  However, that won't typecheck since Q expects an argument of type `P b`, but
  we feed it an argument of type `P a`.
  We need to rewrite a to b using the equality from the implication's antecedence
  somehow.

  Here's how:
*)
Axiom ax : forall (pa: P a) (e: a = b), Q (match e in (eq _ y) return (P y) with
  | eq_refl => pa
end).

(* shorter with some notations: *)
Import EqNotations.
Axiom ax' : forall (pa: P a) (e: a = b), Q (rew e in pa).