# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1402472840 -32400
# Node ID fe231950824ae8e382bb13439582b3a5b6f8bdc9
# Parent  ca278492b95f5f6c76f0e8f680403c6ebc189fe4
Define not in SystemT

diff -r ca278492b95f -r fe231950824a systemF.agda
--- 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))