Prefixed enumeration literals not correctly handled in proofs

[treiher]

Example

   type Message is
      message
         Tag    : Tag
            then Length
               if Tag = TLV.Msg_Data,
            then null
               if Tag = TLV.Msg_Error;
         Length : Length
            then Value
               with Length => Length * 8;
         Value  : Opaque;
       end message;

specs/tlv.rflx:8:10: model: error: conflicting conditions for field "Tag"
specs/tlv.rflx:10:19: model: info: condition 0 (Tag -> Length): Tag = TLV.Msg_Data
specs/tlv.rflx:12:19: model: info: condition 1 (Tag -> Final): Tag = TLV.Msg_Error