DEFINITION A_rect()
TYPE =
       ΠP:A
                →(Type:92577:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs/A_rect.con)
         .Πn:nat.Πn1:nat.(P (ASort n n1))
           →(Πa:A.(P a)→Πa1:A.(P a1)→(P (AHead a a1))
                →Πa:A.(P a))
BODY =
Show proof