proposition: Theorem eval_P: forall p a, P a -> (forall i, In i p -> P i) -> P (eval p a).
proof: Proof. intros p a Pa; elim p; simpl; auto with datatypes. intros a1 l1 Rec H; apply Pplus; auto. Qed.
imports: ZArith List UList Tactic Permutation