INDUCTIVE DEFINITION aprem () [ ]
OF ARITY nat→A→A→Prop
BUILT FROM:
     aprem_zero: ∀a1:A.∀a2:A.(aprem O (AHead a1 a2) a1)
   | aprem_succ: ∀a2:A.∀a:A.∀i:nat.(aprem i a2 a)→∀a1:A.(aprem (S i) (AHead a1 a2) a)