Definition fst_eq

Definition. fst_eq
fst t = ⋂⋂t

Projection on the first component of a Kuratowski pair, see pair_fst.