diff options
-rw-r--r-- | lib/Maps.v | 6 |
1 files changed, 0 insertions, 6 deletions
@@ -1125,12 +1125,6 @@ Module EMap(X: EQUALITY_TYPE) <: MAP. Proof. intros. unfold get, map. reflexivity. Qed. - Lemma exten: - forall (A: Set) (m1 m2: t A), - (forall x: X.t, m1 x = m2 x) -> m1 = m2. - Proof. - intros. unfold t. apply extensionality. assumption. - Qed. End EMap. (** * Useful notations *) |