proposition: Theorem PCond_app l l1 l2 : PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2.
proof: Proof. induction l1 as [|a l1 IHl1]. - simpl. split; [split|destruct 1]; trivial. - simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc. Qed.
imports: ZArith_base