Make a general inductive construction framework
It would be convenient for future uses, and if we want to implement general inductives in our theory in the future, to implement a framework to construct inductives given it's constructors, the following instructions should serve as a first step towards writing one:
// We assume for now that inductive are non-indexed, non nested and have large elimination
// if the inductive has n constructors c1,...,cn, then the recursor will be of the form:
// a_rec.{u} : (motive : a -> Sort u) -> p1 -> ... -> pn -> (a : a) -> motive a
// where pi :
// (a1 : T1) -> ... -> (ak : Tk) -> ((motive ai)) -> motive (cn a1 ... ak)
// where ((motive ai)) is the chain of (motive ai) where ai is a recursive argument.
// For example :
// ```
// inductive Tree :
// | nil : Tree
// | cons : Nat -> Tree -> Tree -> Tree
// ```
// Tree has two constructors, nil and succ,
// nil has no arguments and 0 recursive args
// cons has 3 arguments [a1 : Nat, a2 : Tree, a3 : Tree], with two recursive args [a2,a3]
// thus, the recursor is formed as follows:
// Tree_rec.{u} :
// (motive : Tree -> Sort u)
// -> motive nil
// -> ((a1 : Nat) -> (a2 a3 : tree) -> motive a2 -> motive a3 -> motive (cons a1 a2 a3))
// -> (a : Tree) -> motive a
// For reduction, we proceed as such
// when encountering a recursor, we first check that the number of arguments given is
// n+2 (as in, the rec is imbricked in n+2 App constructors)
// We then put the last argument given in head normal-form (not whnf, we want to unfold definitions here !)
// and see if his head is a constructor. If it is a certain (ci a1 ... ak), we pick the i+1nth argument of n_rec pi and reduce what we have to
// a_rec motive ((pi)) (ci a1 ... ak)
// => pi a1 ... ak ((a_rec motive ((pi)) ai))