fact: Fixpoint foo_depth f := match f with | Foo1 => 0 | Foo2 f => 1 + foo_depth f | Foo3 n f => 1 + foo_depth f end.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads