nominal key_certified = ()
nominal leader_elected = ()
nominal epoch_21 = ()
nominal epoch_22 = ()
nominal committee_9 = ()
nominal validator_17 = ()
nominal group_key committee epoch = string
nominal ssle_ticket validator committee epoch = string
nominal leader_certificate validator committee epoch = string

union dkg_ssle_op from to result =
    | ElectLeader :: forall validator committee epoch.
        group_key committee epoch * ssle_ticket validator committee epoch ->
        dkg_ssle_op key_certified leader_elected (leader_certificate validator committee epoch)

inl elect_epoch_22
    (key : group_key committee_9 epoch_22)
    (ticket : ssle_ticket validator_17 committee_9 epoch_22)
    : leader_certificate validator_17 committee_9 epoch_22 =
    match ElectLeader (key, ticket) with
    | ElectLeader _ => leader_certificate "leader-17"

inl main () : leader_certificate validator_17 committee_9 epoch_22 =
    inl key : group_key committee_9 epoch_22 = group_key "group-key-9-22"
    inl stale : ssle_ticket validator_17 committee_9 epoch_21 = ssle_ticket "stale-ticket"
    elect_epoch_22 key stale