Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).