DEFINITION G_rect()
TYPE =
       ΠP:G
                →(Type:92143:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G_rect.con)
         .Πf:nat→nat.ΠH:∀n:nat.(lt n (f n)).(P (mk_G f H))
           →Πg:G.(P g)
BODY =
Show proof