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 =
Show proof