proposition: Theorem PFcons2_fcons_inv: forall l a l1, PCond l (Fcons2 a l1) -> ~ a @ l == 0 /\ PCond l l1.
proof: Proof. unfold Fcons2; intros l a l1 H; split; case (PFcons1_fcons_inv l (PEsimp a) l1); trivial. intros H1 H2 H3; case H1. transitivity (a@l); trivial. apply PEsimp_ok. Qed.
imports: ZArith_base