Load removeNonAug.

Inductive listáµ— (A : Type) (Aáµ— : A -> Type) : list A -> Type :=
    niláµ— : listáµ— A Aáµ— []
  | consáµ— : forall H : A,
            Aáµ— H -> forall H0 : list A, listáµ— A Aáµ— H0 -> listáµ— A Aáµ— (H :: H0).

Inductive booláµ— : bool -> Set :=
  trueáµ— : booláµ— true | falseáµ— : booláµ— false.
Inductive natáµ— : nat -> Set :=
    Oáµ— : natáµ— 0
  | Sáµ— : forall H : nat, natáµ— H -> natáµ— (S H).

Definition vec := VectorDef.t.

Inductive
vecáµ— (A : Type) (Aáµ— : A -> Type)
  : forall H : nat, natáµ— H -> vec A H -> Type :=
    vecniláµ— : vecáµ— A Aáµ— 0 Oáµ— (@Vector.nil A)
  | vecconsáµ— : forall H : A,
               Aáµ— H ->
               forall (n : nat) (náµ— : natáµ— n)
                 (H0 : vec A n),
               vecáµ— A Aáµ— n náµ— H0 ->
               vecáµ— A Aáµ— (S n) (Sáµ— n náµ—)
                    (@Vector.cons A H n H0).

(* Inductive *)
(* vecáµ—' (A : Type) (Aáµ— : A -> Type) *)
(*   : forall H : nat, vec A H -> Type := *)
(*     vecniláµ—' : vecáµ—' A Aáµ— 0 (@Vector.nil A) *)
(*   | vecconsáµ—' : forall H : A, *)
(*                Aáµ— H -> *)
(*                forall (n : nat) *)
(*                (1* (náµ— : natáµ— n) *1) *)
(*                  (H0 : vec A n), *)
(*                vecáµ—' A Aáµ— n H0 -> *)
(*                vecáµ—' A Aáµ— (S n) *)
(*                     (@Vector.cons A H n H0). *)

(*
Print vecáµ—.

Inductive
vecáµ— (A : Type) (Aáµ— : A -> Type)
  : forall H : nat, natáµ— H -> vec A H -> Type :=
    vecniláµ— : vecáµ— A Aáµ— 0 Oáµ— (Vector.nil A)
  | vecconsáµ— : forall H : A,
               Aáµ— H ->
               forall (n : nat) (náµ— : natáµ— n) (H0 : vec A n),
               vecáµ— A Aáµ— n náµ— H0 ->
               vecáµ— A Aáµ— (S n) (Sáµ— n náµ—) (Vector.cons A H n H0)
               *)

(* MetaCoq Run (cleanInd "vecáµ—" >>= tmMsg). *)
(* MetaCoq Run (cleanInd listáµ— >>= tmMsg). *)

(* Print vecáµ—0. *)
(* Print listáµ—0. *)

Print tmMkInductive.
Print mutual_inductive_entry.
Search mutual_inductive_entry.
Print mutual_inductive_body.
Print context_decl.

MetaCoq Run (tmQuoteInductive "vecáµ—" >>= tmPrint).

Compute (removeArgList (tApp (tRel 0) [tRel 1;tRel 2;tRel 3]) [1]).

About print_term.
Search global_env_ext.

(* MetaCoq Run ( *)
(* xp <- removeNonAugmentable <*)
(*   , forall H : nat, natáµ— H -> vec A H -> Type *)
(* y <- tmEval all (xp);; *)
(* tmPrint y;; *)
(* tmMsg (print_term (empty_ext )  true y.1)). *)

(* MetaCoq Run ( *)
(* x <- removeNonAugmentable *)
(*   <*)
(* forall(A : Type) (Aáµ— : A -> Type), *)
(*                forall H : A, *)
(*                Aáµ— H -> *)
(*                forall (n : nat) (náµ— : natáµ— n) *)
(*                  (H0 : vec A n), *)
(*                vecáµ— A Aáµ— n náµ— H0 -> *)
(*                vecáµ— A Aáµ— (S n) (Sáµ— n náµ—) *)
(*                     (@Vector.cons A H n H0) *)
(*   *)
(* y <- tmEval all (x);; *)
(* tmPrint y;; *)
(* tmMsg (print_term (empty_ext )  true y.1);; *)
(* tmMsg "";; *)
(* tmMsg "";; *)
(* tmMsg "";; *)
(* y2 <- tmEval all (removeArgList (y.1) 3);; *)
(* tmPrint y2;; *)
(* tmMsg (print_term (empty_ext )  true y2) *)
(* ). *)

(*
1. remove Parameter after non augmentable inductive
2. delete parameter in recursive call

should the function look inside the arguments?
TODO: find examples like (T -> nat) or (nat -> T) in an argument
*)