fact: Definition beth x := let p := fun z => \2c ^c z in let osup := fun y f => \osup (fun_image y (fun z => (p (f z)))) in let osupp:= fun f => Yo (domain f = \0o) omega0 (osup (domain f) (Vg f)) in let f:= transdef_ord osupp in f x.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)