DEFINITION A_ind()
TYPE =
       ∀P:A→Prop
         .∀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