DEFINITION A_rec()
TYPE =
       ΠP:A→Set
         .Π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→Set
         .λ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)
               }