module test
-import T
+import StdEnv
-Start = dynamic someT
+:: Exist = E.e: Ex e & TC e & == e
+
+Start = Ex 42 == Ex 42
+
+instance == Exist
+where
+ (==) (Ex e1) (Ex e2) = dynEq (dynamic e1) e2
+
+dynEq :: Dynamic -> (a -> Bool) | TC, == a
+dynEq (a :: a^) = (==) a
+dynEq _ = const False