bType {
      sub_sort :> Type;
      val : sub_sort -> T;
      Sub : forall x, P x -> sub_sort;
      (* elimination rule for sub_sort *)
      _ : forall K (_ : forall x Px, K (@Sub x Px)) u, K u;
      _ : forall x Px, val (@Sub x Px) = x
    }.
  End SubTypeKit.

  Notation "[ 'subType' 'for' v ]" := (SubType _ v _
    (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px)
    (fun x px => erefl x)).
End Chapter721.

Module Chapter722.
  Theorem eq_irrelevance (T : eqType) (x y : T) : forall e1 