#V #T #H lapply (H T ?) -H /2 width=1/ #H
@(discr_tpair_xy_y โฆ H)
qed-.
(* Basic properties *********************************************************)
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@(discr_tpair_xy_y โฆ H)
qed-.
(* Basic properties *********************************************************)