From 94f965baf3483552b1f95c9a5ba92a99a5eb8c7f Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 1 Nov 2021 14:29:53 +0100
Subject: [PATCH] Add injectivity/equality axiom

---
 src/main/universal/res/config/prelude.sil | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/main/universal/res/config/prelude.sil b/src/main/universal/res/config/prelude.sil
index b10eaa9a58..d477eba6b0 100644
--- a/src/main/universal/res/config/prelude.sil
+++ b/src/main/universal/res/config/prelude.sil
@@ -62,6 +62,10 @@ domain VCTOption[T] {
     forall x: T :: {VCTSome(x)} VCTNone() != VCTSome(x)
   }
 
+  axiom equal_vct {
+    forall x: T, y: T :: {VCTSome(x), VCTSome(y)} (VCTSome(x) == VCTSome(y)) == (x == y)
+  }
+
   axiom get_axiom_vct {
     forall x: T :: {getVCTOption(VCTSome(x))} getVCTOption(VCTSome(x)) == x
   }