comparison systemT.agda @ 3:7138e79615b3

Proof add-sym
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 21 May 2014 14:41:45 +0900
parents ca2e9f7a7898
children
comparison
equal deleted inserted replaced
2:ca2e9f7a7898 3:7138e79615b3
13 R u v (S t) = v (R u v t) t 13 R u v (S t) = v (R u v t) t
14 14
15 D : {U : Set} -> U -> U -> Bool -> U 15 D : {U : Set} -> U -> U -> Bool -> U
16 D u v F = v 16 D u v F = v
17 D u v T = u 17 D u v T = u
18