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 =
λP:G
               →(Type:92143:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G_rect.con)
         .λ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