Give an explicit name in a proof

Very slightly improves the style of the proof.
coq-community · Feb 6, 2021 · bea59b7 · bea59b7
1 parent 621fa26
commit bea59b7
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/Topology/Neighborhoods.v b/theories/Topology/Neighborhoods.v
@@ -24,10 +24,10 @@ Lemma neighborhood_interior: forall {X:TopologicalSpace}
   neighborhood N x -> In (interior N) x.
 Proof.
 intros.
+destruct H as [U].
 destruct H.
 destruct H.
-destruct H.
-assert (Included x0 (interior N)) by
+assert (Included U (interior N)) by
   now apply interior_maximal.
 auto with sets.
 Qed.