Definition fst_eq
Definition.
fst_eq
fst t = ⋂⋂t
Projection on the first component of a
Kuratowski pair
, see
pair_fst
.