幻に終わった愛の教団

gistfile1.v

Section CultOfLoveDoesNotExist.

Variable human : Set.
Variable P : human -> Prop. (* xは愛の教団に属する *)
Variable L : human -> human -> Prop. (* xはyを愛する *) 

Theorem CultOfLoveDoesNotExist
 (forall x : human, P x -> forall y : human, ~ L y y -> L x y) /\
 (forall x : human, P x -> forall y : human, L x y -> ~ L y y) ->
 ~ (exists x : human, P x).
Proof.
unfold not.
intros.
destruct H0.
destruct H.
apply (H1 x H0 x); apply (H x H0 x); intros; apply (H1 x H0 x); assumption.
Qed.

End CultOfLoveDoesNotExist.