(VAR Fa Fb Fu Ga Gb Gu Ha Hb Hu X Y Z x y )
(RULES 
        casea(inl(X), Fa, Ga) -> 
        casea(inr(Y), Fa, Ga) -> 
        casea(Z, , ) -> 
        caseb(inl(X), Fb, Gb) -> 
        caseb(inr(Y), Fb, Gb) -> 
        caseb(Z, , ) -> 
        caseu(inl(X), Fu, Gu) -> 
        caseu(inr(Y), Fu, Gu) -> 
        caseu(Z, , ) -> 
        
)