矛盾

楚人に盾と矛とを鬻（ひさ）ぐ者有り。之（これ）を誉めて（ほめて）曰く「吾が盾の堅きこと、能く（よく）陥す（とほす）もの莫し（なし）」と。また、その矛をほめていはく、「わが矛の利なること、物において陥（とほ）さざることなきなり。」と。あるひといはく、「子の矛を以て、子の盾を陥（とほ）さばいかん。」と。その人応ふること能はざりき。

矛盾 - Wikipedia

Theorem 矛盾 : forall (矛 盾:Type)(突き通す:矛 -> 盾 -> Prop),
 (exists 最強の矛:矛, forall あらゆる盾:盾, 突き通す 最強の矛 あらゆる盾) ->
 (exists 最強の盾:盾, forall あらゆる矛:矛, ~ 突き通す あらゆる矛 最強の盾) ->
 False.
Proof.
 intros 矛 盾 突き通す.
 intros どんな盾でも貫く矛がある どんな矛でも防ぐ盾がある.
 elim どんな盾でも貫く矛がある.
 intros 最強の矛 最強の矛はあらゆる盾を貫く.
 elim どんな矛でも防ぐ盾がある.
 intros 最強の盾 最強の盾はあらゆる矛を防ぐ.
 apply (最強の盾はあらゆる矛を防ぐ 最強の矛).
 apply (最強の矛はあらゆる盾を貫く 最強の盾).
Qed.