Takafumi Saikawa

Do we need to keep both? ``` Lemma at_pointE T (t : T) : at_point t = principal_filter t. Proof. by apply:funext=> S; apply: propext; split=> [? ? -> |...