//qualif NonNull(v: [a])        : (? (nonnull([v])))
//qualif Null(v: [a])           : (~ (? (nonnull([v]))))
//qualif EqNull(v:Bool, ~A: [a]): (v <=> (? (nonnull([~A]))))

// qualif IsEmp(v:GHC.Types.Bool, ~A: [a]) : ((v) <=> len([~A]) [ > ;  = ] 0)
// qualif ListZ(v: [a])          : len([v]) [ = ; >= ; > ] 0 
// qualif CmpLen(v:[a], ~A:[b])  : len([v]) [= ; >=; >; <=; <] len([~A]) 
// qualif EqLen(v:int, ~A: [a])  : v = len([~A]) 
// qualif LenEq(v:[a], ~A: int)  : ~A = len([v]) 
// qualif LenAcc(v:int, ~A:[a], ~B: int): v = len([~A]) + ~B
// qualif LenDiff(v:[a], ~A:int): len([v]) = (~A [ +; - ] 1)

qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0))
qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0))

qualif ListZ(v: [a])          : (len([v]) =  0) 
qualif ListZ(v: [a])          : (len([v]) >= 0) 
qualif ListZ(v: [a])          : (len([v]) >  0) 

qualif CmpLen(v:[a], xs:[b])  : (len([v]) =  len([xs])) 
qualif CmpLen(v:[a], xs:[b])  : (len([v]) >= len([xs])) 
qualif CmpLen(v:[a], xs:[b])  : (len([v]) >  len([xs])) 
qualif CmpLen(v:[a], xs:[b])  : (len([v]) <= len([xs])) 
qualif CmpLen(v:[a], xs:[b])  : (len([v]) <  len([xs])) 

qualif EqLen(v:int, xs: [a])  : (v = len([xs])) 
qualif LenEq(v:[a], x: int)   : (x = len([v])) 
qualif LenDiff(v:[a], x:int)  : (len([v]) = x + 1)
qualif LenDiff(v:[a], x:int)  : (len([v]) = x - 1)
qualif LenAcc(v:int, xs:[a], n: int): (v = len([xs]) + n)