proposition: Lemma fcons_ok : forall l l1, (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
proof: Proof. intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. induction l1 as [|a l1 IHl1]; simpl; intros. - trivial. - elim PCond_fcons_inv with (1 := H); intros. destruct l1; trivial. split; trivial. apply IHl1; trivial. Qed.
imports: ZArith_base