Set Debug "backtrace".
Set Debug "generate_eliminators".

(* Preliminary to be testable without the prelude *)
Notation "A -> B" := (forall (_ : A), B) (right associativity, at level 99).

(* This needs to be registered *)
Inductive unit : Set :=
    tt : unit.

Register unit as core.unit.type.
Register tt as core.unit.tt.

Inductive prod (A B : Type) : Type :=
pair : A -> B -> prod A B.

Arguments pair {_ _}.

#[universes(polymorphic)]
Inductive prod_all@{sa sb ; ua ub +} A (PA : A -> Type@{sa;ua}) B (PB : B -> Type@{sb;ub}) : prod A B -> Type :=
pair_all : forall a, PA a -> forall b, PB b -> prod_all A PA B PB (pair a b).

#[universes(polymorphic)]
Definition prod_all_forall@{sa sb ; ua ub +} A (PA : A -> Type@{sa;ua}) (HPA : forall a, PA a)
                    B (PB : B -> Type@{sb;ub}) (HPB : forall b, PB b) :
                    forall (x : prod A B), prod_all A PA B PB x :=
fun x => match x with
| pair a b => pair_all A PA B PB a (HPA a) b (HPB b)
end.

Register Scheme prod_all as All for prod.
Register Scheme prod_all_forall as AllForall for prod.

Variant Box (F  : unit -> Type) := .

Inductive Cut (x : unit) : Type :=
| triv : Box (fun n => prod (Cut n) unit) -> Cut x.