Require Import Reals Utf8.
Set Implicit Arguments.
Open Scope R.

Fixpoint type_pow (n: nat) (x: Type): Type :=
  match n with
  | O => x
  | S m => prod (type_pow m x) x
  end.

Definition derivative (i: nat): (R -> R) -> (R -> R).
Proof. Admitted.

Definition implicit_general_ODE (n: nat): (type_pow (S (S n)) R -> R) -> (R -> R) -> Prop.
Proof.
  intros F x. refine (∀ (t: R), _: Prop).
  induction n.
  + simpl in *. exact (F (t, x t, (derivative 1%nat x) t) = 0).
  + simpl in *. pose ((derivative (S (S n)) x) t) as x'. exact (IHn (λ t, F (t, x'))).
Defined.

Definition test: type_pow 3%nat R -> R.
Proof.
  intros [[[x y] z] w]. simpl in *. exact (x + y + z + w).
Defined.

Eval compute in (implicit_general_ODE test).