DEFINITION G_rec()
TYPE =
       ΠP:G→Set
         .Πf:nat→nat.ΠH:∀n:nat.(lt n (f n)).(P (mk_G f H))
           →Πg:G.(P g)
BODY =
Show proof