24/04/12 11:38:22.83 VfOiBAdh.net
>>24
False型の値を返すと、Falseが証明される
False型の値はない（FalseはType型の値）ので、真の命題からは返すことはできない
唯一返すことができるのは、仮定もFalseである場合のみ
これはXから∅への写像の集合
∅^X := {f: X -> ∅}
が、X = ∅のときのみ元を1個持ち、その他の時は空集合であることに対応
24/04/12 11:38:22.83 VfOiBAdh.net
>>24
False型の値を返すと、Falseが証明される
False型の値はない（FalseはType型の値）ので、真の命題からは返すことはできない
唯一返すことができるのは、仮定もFalseである場合のみ
これはXから∅への写像の集合
∅^X := {f: X -> ∅}
が、X = ∅のときのみ元を1個持ち、その他の時は空集合であることに対応