Section うみねこ8のメモ.
Definition Pow (S : Set) : Type := S -> Prop.
Variable Animal : Set.
Definition animal (a : Animal) : Prop := True.
Variable human : Pow Animal.
Axiom 人間は1人はいてはる : exists h : Animal , human h.
Theorem 人間は動物 : forall (x : Animal) , human x -> animal x.
Proof.
intro a.
intro a_is_human.
unfold animal.
auto.
Qed.
Hypothesis アッ動物は人間じゃない : forall (x : Animal) , animal x -> ~(human x).
Theorem アッ人間は動物じゃない : forall (x : Animal) , human x -> ~(animal x).
Proof.
intros x xishuman xisanimal.
apply (アッ動物は人間じゃない x xisanimal).
auto.
Qed.
Variable P : Prop.
Theorem inconsistency : P.
Proof.
destruct 人間は1人はいてはる.
assert (animal x) as xは動物.
apply 人間は動物.
auto.
assert (~ animal x) as xは動物とちがう.
apply アッ人間は動物じゃない.
auto.
apply False_ind.
apply xは動物とちがう.
apply xは動物.
Qed.
End うみねこ8のメモ.
