--- a/systemF.agda	Wed Jun 11 16:41:01 2014 +0900
+++ b/systemF.agda	Wed Jun 11 16:47:20 2014 +0900
@@ -13,6 +13,9 @@
 F : Bool
 F = \{X : Set} -> \x -> \(y : X) -> y
 
+not : Bool -> Bool
+not b =  \{X : Set} -> \(x : X) -> \(y : X) -> b y x
+
 D : {X : Set} -> (U V : X) -> Bool -> X
 D {X} u v bool = bool {X} u v
 
@@ -22,6 +25,9 @@
 lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
 lemma-bool-f = refl
 
+lemma-bool-not-D : {X : Set} {u v : X} {b : Bool} -> D u v b ≡ D v u (not b)
+lemma-bool-not-D = refl
+
 -- Product
 
 _×_ : ∀ {l ll} -> Set l -> Set ll -> {lll : Level} -> Set (suc lll ⊔ (ll ⊔ l))