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 =
λP:A
               →(Type:92577:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs/A_rect.con)
         .λf:Πn:nat.Πn1:nat.(P (ASort n n1))
           .λf1:Πa:A.(P a)→Πa1:A.(P a1)→(P (AHead a a1))
             .FIXaux{
               aux:Πa:A.(P a)
               :=λa:A.<P> CASE a OF ASort n n1⇒f n n1 | AHead a1 a2⇒f1 a1 (aux a1) a2 (aux a2)
               }