data False = 

(+) (A,B:: Set)
    :: Set
    = data inl (a:: A) | inr (b:: B)


postulate A :: Set
postulate EqA :: A -> A -> Set
postulate B :: Set
postulate EqB :: B -> B -> Set

AB :: Set
   = A + B


EqAB :: AB -> AB -> Set
      =  \(ab,ab'::AB)-> 
         case ab of
         (inl a)-> case ab' of
                   (inl a')->  EqA a a'
                   (inr b')->  False
         (inr b)-> case ab' of
                   (inl a')-> False
                   (inr b')-> EqB b b'



SymA :: Set
     = (a,a':: A) -> EqA a a' -> EqA a' a



SymB :: Set
     = (b,b':: B) -> EqB b b' -> EqB b' b


SymAB :: Set
      = (ab,ab':: AB) -> EqAB ab ab' -> EqAB ab' ab


symAB (symA :: SymA)
      (symB :: SymB)
      :: SymAB
      = \(ab,ab'::AB)-> 
        \(abab'::EqAB ab ab')-> 
        case ab of
        (inl a)-> case ab' of
                  (inl a')-> symA a a' abab'
                  (inr b )-> case abab' of { }
        (inr b)-> case ab' of
                  (inl a )-> case abab' of { }
                  (inr b')-> symB b b' abab'


symAB' (symA :: SymA)
       (symB :: SymB)
       :: SymAB
       = \(ab,ab'::AB)-> 
         \(abab'::EqAB ab ab')-> 
         case ab of
         (inl a)-> case ab' of
                   (inl a')-> symA a a' abab'
                   (inr b )-> abab'
         (inr b)-> case ab' of
                   (inl a )-> abab'
                   (inr b')-> symB b b' abab'