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 =
Show proof