Как определить индуктивный тип, взаимно рекурсивный с функцией?

Я хочу определить индуктивный тип Foo, с конструкторами, принимающими в качестве аргументов некоторые свойства. Я хочу, чтобы эти свойства зависели от индуктивных аргументов того типа, который я сейчас определяю. Я хочу иметь возможность собирать некоторые данные от них внутри этих свойств, используя некоторую рекурсивную функцию bar, которая будет принимать объект типа Foo. Однако я не знаю, как объявить этих двоих, чтобы Coq принял их определения. Я хочу написать что-то вроде этого:

Inductive Foo : Set (* or Type *) :=
| Foo1 : forall f : Foo, bar f = 1 -> Foo
| Foo2 : forall f : Foo,  bar f = 2 -> Foo
| Foon : nat -> Foo
with bar (f : Foo) : nat := 
  match f with
  | Foo1 _ _ => 1
  | Foo2 _ _ => 2
  | Foon n => S n
  end.

Обычно with - это способ обработки взаимной рекурсии, однако все примеры, которые я видел, когда он использовался с обоими определениями, начинаются либо с Inductive, либо с обоими Fixpoint. Возможна ли вообще такая взаимная рекурсия?