proposition: Theorem PFcons_fcons_inv: forall l a l1, PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1.
proof: Proof. intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons. - simpl; now split. - case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2); repeat split; trivial. + now rewrite H. + now apply IHl1. + now apply IHl1. Qed.
imports: ZArith_base