module test

import StdEnv

:: 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