Commit 4ab7caac authored by MARCHE Claude's avatar MARCHE Claude
Browse files

remove axiom set.SetMap.Equal_is_eq: extensionality of equality should

be stated on maps instead. This theory does not seem to be used anyway.
parent 1a1bcbab
......@@ -375,7 +375,9 @@ theory SetMap
predicate equal(s1 s2 : set 'a) = forall x : 'a. s1[x] = s2[x]
(* dubious axiom: extensionality should be postulated on maps instead
axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
predicate subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment