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 =
λP:G→Set
         .λf:Πf:nat→nat.ΠH:∀n:nat.(lt n (f n)).(P (mk_G f H))
           .λg:G.<P> CASE g OF mk_G f1 H⇒f f1 H