@@ -19,6 +19,9 @@ replace refl prf = prf
1919sym : {l:a} -> {r:a} -> l = r -> r = l
2020sym refl = refl
2121
22+trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c
23+trans refl refl = refl
24+
2225lazy : a -> a
2326lazy x = x -- compiled specially
2427