proposition: Lemma not_forall: forall (V:Type)(P : V -> Prop), (exists x : V, ~ P x) -> ~ (forall x : V, P x).
proof: Proof. intros. unfold not. intros. firstorder. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)