(\/) (A,B:: Set)
     :: Set
     = data or1 (a:: A) | or2 (b:: B)


postulate A:: Set
postulate B:: Set

lemma3 (ab ::  A \/ B)
       :: B \/ A
       = case ab of
         (or1 a)->
           or2@_ a
         (or2 b)->
           or1@_ b