DEFINITION G_ind()
TYPE =
       ∀P:G→Prop
         .(∀f:nat→nat.∀H:∀n:nat.(lt n (f n)).(P (mk_G f H)))→∀g:G.(P g)
BODY =
        assume P: G→Prop
        suppose H: ∀f:nat→nat.∀H:∀n:nat.(lt n (f n)).(P (mk_G f H))
        assume g: G
          by cases on g we prove P g
             case mk_G f:nat→nat H1:∀n:nat.(lt n (f n)) ⇒
                the thesis becomes P (mk_G f H1)
                by (H . H1)
P (mk_G f H1)
          we proved P g
       we proved 
          ∀P:G→Prop
            .(∀f:nat→nat.∀H:∀n:nat.(lt n (f n)).(P (mk_G f H)))→∀g:G.(P g)