inductive aprem: nat \to (A \to (A \to Prop)) \def
| aprem_zero: \forall (a1: A).(\forall (a2: A).(aprem O (AHead a1 a2) a1))
inductive aprem: nat \to (A \to (A \to Prop)) \def
| aprem_zero: \forall (a1: A).(\forall (a2: A).(aprem O (AHead a1 a2) a1))