proposition: Lemma level_max (x : T) (lx : x \in lfp) : levl lx < size U.
proof: Proof. rewrite /levl. case: (ex_minnP _) => m m1 m2. move: lx. rewrite /lfp. case: (size U) => //=. by rewrite inE. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)