@@ -35,7 +35,7 @@ sym : {l:a} -> {r:a} -> l = r -> r = l
35sym refl = refl
35sym refl = refl
37||| Transitivity of propositional equality
37||| Transitivity of propositional equality
38−trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c
38+trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
39trans refl refl = refl
39trans refl refl = refl
41lazy : a -> a
41lazy : a -> a