[Broke out some definitions which simplify calculations.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080207022158] addfile ./Derivation.agda
hunk ./Derivation.agda 1
+-- Some definitions which simplify the calculations done elsewhere.
+
+module Derivation where
+
+open import Logic
+
+EqualTo : {a : Set} (x : a) -> Set
+EqualTo x = ∃₀ (\y -> x ≡ y)
+
+infix 0 ▷_
+
+▷_ : forall {a} {x y : a} -> x ≡ y -> EqualTo x
+▷_ = exists
hunk ./HuttonsRazor.agda 21
+open import Derivation
hunk ./HuttonsRazor.agda 114
-EqualTo : {a : Set} (x : a) -> Set
-EqualTo x = ∃₀ (\y -> x ≡ y)
-
-infix 0 ▷_
-
-▷_ : forall {a} {x y : a} -> x ≡ y -> EqualTo x
-▷_ = exists
-