It is a bit difficult to figure out what you would like to compute as you event type, is effectively, not inhabited. Apart from these considerations, I'd try something like:

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import bigop.

Definition max_seq l := \max_(x <- l) x.

Inductive event : Type :=
  node : seq event -> event.

Fixpoint round_lvl (e : event) : nat :=
  (* XXX: Missing condition *)
  let cond_inc x := round_lvl x in
  match e with
  | node l => max_seq (map cond_inc l)
  end.

But I had trouble parsing what the existence condition means. I suggest you try to express the problem without Coq code first, and maybe from that a solution pops.

It was a bit difficult for me to figure out what you would like to compute, I'd start with something like:

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import bigop.

Definition max_seq l := \max_(x <- l) x.

Inductive event : Type :=
  node : seq event -> event.

Fixpoint round_lvl (e : event) : nat :=
  (* XXX: Missing condition *)
  let cond_inc x := round_lvl x in
  match e with
  | node l => max_seq (map cond_inc l)
  end.

But I had trouble parsing what the existence condition means. I suggest you try to express the problem without Coq code first, and maybe from that a solution pops.