+ module Data.Alphabet
+
+ import Control.SUSY
+ import Control.Total
+ import Data.SUSY
+
+ export
+ (Super a, Super b) => Super (a,b) where
+ deg (x, y) = deg x + deg y
+
+ export
+ [SL] (Letter a, Ord b) => Ord (a,b) where
+ compare (x, xx) (y, yy) with (compare x y)
+ _ | EQ with (deg x)
+ _ | Boson = compare xx yy
+ _ | Fermion = contra $ compare xx yy
+ _ | t = t
+
+ (Letter a, AntiSym b) => AntiSym (a,b) using SL where
+ antisym (x, xx) (y, yy) with (compare x y) proof p
+ _ | LT = rewrite antisym y x in rewrite p in Refl
+ _ | EQ with (deg x) proof pp
+ _ | Boson = rewrite antisym y x in rewrite p in rewrite sym $ degeq x y {p=p} in rewrite pp in antisym xx yy
+ _ | Fermion = rewrite antisym y x in rewrite p in rewrite sym $ degeq x y {p=p} in rewrite pp in rewrite antisym xx yy in Refl
+ _ | GT = rewrite antisym y x in rewrite p in Refl
+