@@ -19,6 +19,9 @@ replace refl prf = prf
19sym : {l:a} -> {r:a} -> l = r -> r = l
19sym : {l:a} -> {r:a} -> l = r -> r = l
20sym refl = refl
20sym refl = refl
22+trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c
23+trans refl refl = refl
22lazy : a -> a
25lazy : a -> a
23lazy x = x -- compiled specially
26lazy x = x -- compiled specially