djspiewak · December 21, 2016 19:39
diff --git a/cps-implication.txt b/cps-implication.txt
 assume: () -> a

 True -> a
 not True \/ a
 False \/ a
 a \/ False
 not a -> False
 (a -> False) -> False

 True = ()
 False = ⊥

 ------ thus

 (() -> a) <-> (a -> ⊥) -> ⊥
	assume: () -> a

	True -> a
	not True \/ a
	False \/ a
	a \/ False
	not a -> False
	(a -> False) -> False

	True = ()
	False = ⊥

	------ thus

	(() -> a) <-> (a -> ⊥) -> ⊥