proposition: Lemma P_neq_not_P: forall (P:Prop), P <> ~P.
proof: Proof. unfold not; intros. assert (~P). unfold not; intro. assert (P->False). rewrite <- H. assumption. tauto. assert P. rewrite H. assumption. tauto. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec