[Updated code to reflect changes in the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080710184614] {
hunk ./SimplyTyped/Semantics/Lemmas.agda 19
-    infixr 2 _⇛⟨_⟩_ _⟶⟨_⟩_
+    infixr 2 _⇛⟨_⟩_
hunk ./SimplyTyped/Semantics/Lemmas.agda 25
-    _⟶⟨_⟩_ : forall x {y z} ->
-             x ⟶ y -> y IsRelatedTo z -> x IsRelatedTo z
-    t₁ ⟶⟨ t₁⟶t₂ ⟩ t₂⇛⋆t₃ = t₁ ⇛⟨ red • t₁⟶t₂ ⟩ t₂⇛⋆t₃
-
}