diff --git a/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs b/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs
index 7d3e1ba4..1674dfc4 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs
@@ -16,6 +16,8 @@ data ParserCode
   | UnknownCommand
   | UnknownModifiers
   | UnknownMode
+  | DuplicateDefinition
+  | DuplicateField
   | ExpectedErrorNotReached
   deriving (Eq, Ord)
 
@@ -30,5 +32,7 @@ parserCodeTable =
     , (UnknownCommand, CodeMeta 5 SError Nothing)
     , (UnknownModifiers, CodeMeta 6 SError Nothing)
     , (UnknownMode, CodeMeta 7 SError Nothing)
-    , (ExpectedErrorNotReached, CodeMeta 8 SError Nothing)
+    , (DuplicateDefinition, CodeMeta 8 SError Nothing)
+    , (DuplicateField, CodeMeta 9 SError Nothing)
+    , (ExpectedErrorNotReached, CodeMeta 10 SError Nothing)
     ]
diff --git a/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs b/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs
index 7fb17ef0..3f2d24c6 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs
@@ -5,6 +5,7 @@
 
 module Coln.Frontend.Parser.Expr where
 
+import Control.Monad (when)
 import Data.List.NonEmpty (NonEmpty (..))
 import FNotation (Ntn)
 import FNotation qualified as N
@@ -85,6 +86,20 @@ fieldSetting e (N.Infix (N.Ident x sp) (N.Keyword ":=" _) body) =
   Record.FieldSetting x <$> chk e body <*> pure sp
 fieldSetting e n = unexpectedNotation e n "field setting of the form `<fieldname> := <expr>`"
 
+recordFields :: ParserEnv -> (Ntn -> IO a) -> [Ntn] -> IO [a]
+recordFields e parseField = go []
+ where
+  go _ [] = pure []
+  go seen (n : rest) = do
+    field <- parseField n
+    seen' <- case n of
+      N.Infix (N.Ident x sp) _ _ -> do
+        when (x `elem` seen) $
+          failWith e sp DuplicateField ("duplicate record field" <+> dpretty x)
+        pure (x : seen)
+      _ -> pure seen
+    (field :) <$> go seen' rest
+
 ident :: ParserEnv -> Ntn -> IO Name
 ident _ (N.Ident x _) = pure x
 ident e n = unexpectedNotation e n "identifier"
@@ -152,10 +167,10 @@ expr e n = case n of
               <*> syn e "term in equality" rhs
           )
   N.Block "sig" Nothing ns _ -> do
-    t <- Record.formation <$> traverse (fieldDecl e) ns
+    t <- Record.formation <$> recordFields e (fieldDecl e) ns
     fromTypD e (N.span n) t
-  N.Block "struct" Nothing ns s ->
-    FromChk "struct expression" <$> (Record.intro s <$> traverse (fieldSetting e) ns)
+  N.Block "struct" Nothing ns s -> do
+    FromChk "struct expression" <$> Record.intro s <$> recordFields e (fieldSetting e) ns
   N.Int i _ -> pure $ fromSynN $ Builtin.intro $ LitInt i
   N.String s _ -> pure $ fromSynN $ Builtin.intro $ LitString s
   n -> unexpectedNotation e n "expression"
diff --git a/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs b/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs
index 15d35334..5aed113e 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs
@@ -5,6 +5,7 @@
 module Coln.Frontend.Parser.Top where
 
 import Control.Exception (try)
+import Control.Monad (when)
 import Data.Foldable (foldlM, forM_)
 import Data.Functor.Contravariant (contramap)
 import Data.List.NonEmpty (NonEmpty (..))
@@ -42,11 +43,11 @@ argBindings e n@(N.Infix n0 (N.Keyword ":" _) n1) = do
   pure (N.span n, m, xs, a)
 argBindings e n = unexpectedNotation e n "argument binding of the form `<names> : <type>`"
 
-unpackArgs :: ParserEnv -> Ntn -> IO (Name, [(Span, Mode, [AbsEntry], Typ N)])
+unpackArgs :: ParserEnv -> Ntn -> IO (Name, Span, [(Span, Mode, [AbsEntry], Typ N)])
 unpackArgs e (N.Group (xN :| argsN)) = do
   x <- ident e xN
   args <- mapM (argBindings e) argsN
-  pure (x, args)
+  pure (x, N.span xN, args)
 
 withArgs :: (V.HasEvaluation c) => [(Span, Mode, [AbsEntry], Typ N)] -> (Typ N, Chk c) -> (Typ N, Chk c)
 withArgs args base = foldr go base args
@@ -61,23 +62,23 @@ withArgs args base = foldr go base args
   introArg sp (Named name) = Function.intro sp name
   introArg sp Anonymous = Function.intro sp "_"
 
-theory :: ParserEnv -> Ntn -> IO (Name, Typ N, Chk D)
+theory :: ParserEnv -> Ntn -> IO (Name, Span, Typ N, Chk D)
 theory e n = do
   (pat_n, body_n) <- definition e n
-  (name, args) <- unpackArgs e pat_n
+  (name, nameSpan, args) <- unpackArgs e pat_n
   body <- chk e body_n
   let (ty, tm) = withArgs args (Typ $ \_ -> pure $ M.univ TheoryU, body)
-  pure $ (name, ty, tm)
+  pure (name, nameSpan, ty, tm)
 
-def :: ParserEnv -> Ntn -> IO (Name, Typ N, Chk D)
+def :: ParserEnv -> Ntn -> IO (Name, Span, Typ N, Chk D)
 def e n = do
   (head_n, body_n) <- definition e n
   (pat_n, ty_n) <- annot e head_n
-  (name, args) <- unpackArgs e pat_n
+  (name, nameSpan, args) <- unpackArgs e pat_n
   returnTyp <- typ e ty_n
   body <- chk e body_n
   let (ty, tm) = withArgs args (returnTyp, body)
-  pure (name, ty, tm)
+  pure (name, nameSpan, ty, tm)
 
 elabDefinition :: DiagnosticEnv ElaboratorCode -> Globals -> Mode -> (Name, Typ N, Chk D) -> IO (Definition Global)
 elabDefinition e g m (x, ty, tm) = do
@@ -102,36 +103,44 @@ attr e sp ntn = do
   let msg = "invalid attr" <+> dpretty ntn
   failWith e sp UnexpectedNotation msg
 
+checkDuplicateIn :: DiagnosticEnv ColnCode -> OMap Name a -> Name -> Span -> IO ()
+checkDuplicateIn e entries x sp =
+  when (x `OMap.member` entries) $
+    failWith (contramap ParserCode e) sp DuplicateDefinition ("duplicate definition of" <+> dpretty x)
+
 decl :: DiagnosticEnv ColnCode -> Globals -> Ntn -> IO Globals
 decl e g (N.MDecl ms "theory" n sp) = do
   m <- mode (contramap ParserCode e) sp ms
-  (x, t, c) <- theory (contramap ParserCode e) n
+  (x, xsp, t, c) <- theory (contramap ParserCode e) n
+  checkDuplicateIn e g.definitions x xsp
   ge <- elabDefinition (contramap ElaboratorCode e) g m (x, t, c)
   pure $ addDefinition x ge g
 decl e g (N.MDecl ms "def" n sp) = do
   m <- mode (contramap ParserCode e) sp ms
-  (x, t, c) <- def (contramap ParserCode e) n
+  (x, xsp, t, c) <- def (contramap ParserCode e) n
+  checkDuplicateIn e g.definitions x xsp
   ge <- elabDefinition (contramap ElaboratorCode e) g m (x, t, c)
   pure $ addDefinition x ge g
 decl e g (N.Block "realm" (Just head) body _) = do
-  (x, r) <- realm e g head body
+  (x, xsp, r) <- realm e g head body
+  checkDuplicateIn e g.realms x xsp
   pure $ addRealm x r g
 decl e g (N.MDecl ms "attr" n sp) = do
   x <- attr (contramap ParserCode e) sp n
   pure $ pushAttr x g
 decl e _ n = unexpectedNotation (contramap ParserCode e) n "top-level declaration"
 
-realmHead :: ParserEnv -> Ntn -> IO (Name, Ntn)
-realmHead _ (N.Infix (N.Ident x _) (N.Keyword "@" _) n) = pure (x, n)
+realmHead :: ParserEnv -> Ntn -> IO (Name, Span, Ntn)
+realmHead _ (N.Infix (N.Ident x sp) (N.Keyword "@" _) n) = pure (x, sp, n)
 realmHead e n = unexpectedNotation e n "realm head"
 
-realm :: DiagnosticEnv ColnCode -> Globals -> Ntn -> [Ntn] -> IO (Name, Realm)
+realm :: DiagnosticEnv ColnCode -> Globals -> Ntn -> [Ntn] -> IO (Name, Span, Realm)
 realm e g head def_ns = do
-  (x, theory_n) <- realmHead (contramap ParserCode e) head
+  (x, xsp, theory_n) <- realmHead (contramap ParserCode e) head
   theory_typ <- typ (contramap ParserCode e) theory_n
   theory <- theory_typ.elab (emptyElabEnv (contramap ElaboratorCode e) g Inductive)
   defs <- realmDecls e g theory.val def_ns
-  pure (x, Realm theory defs)
+  pure (x, xsp, Realm theory defs)
 
 elabRealmDefinition :: ElabEnv N -> Mode -> (Typ N, Chk D) -> IO (Definition Local)
 elabRealmDefinition e m (ty, tm) = do
@@ -146,7 +155,9 @@ elabRealmDefinition e m (ty, tm) = do
 realmDecl :: DiagnosticEnv ColnCode -> ElabEnv N -> Ntn -> IO (Name, Definition Local)
 realmDecl de e (N.MDecl ms "def" n sp) = do
   m <- mode (contramap ParserCode de) sp ms
-  (x, t, c) <- def (contramap ParserCode de) n
+  (x, xsp, t, c) <- def (contramap ParserCode de) n
+  when (x `elem` e.scope.names) $
+    failWith (contramap ParserCode de) xsp DuplicateDefinition ("duplicate definition of" <+> dpretty x)
   d <- elabRealmDefinition e m (t, c)
   pure (x, d)
 realmDecl de _ n = unexpectedNotation (contramap ParserCode de) n "realm declaration"
diff --git a/packages/coln-compiler/test/golden/multi-pi.coln b/packages/coln-compiler/test/golden/multi-pi.coln
index 73e07570..eef51bb0 100644
--- a/packages/coln-compiler/test/golden/multi-pi.coln
+++ b/packages/coln-compiler/test/golden/multi-pi.coln
@@ -77,8 +77,6 @@ def eq-dep-tail-backward (F : Int -> Set) (f : (^c x : Int) -> (^c y : Int) -> (
 
 ## Bad cases:
 
-def eq-multi-2 : (x y : Int) -> Int := x => y => 19
-
 attr expected-error "E0300"
 def eq-too-few : (x : Int) -> Int := eq-multi-2
 
diff --git a/packages/coln-compiler/test/golden/multi-pi.output b/packages/coln-compiler/test/golden/multi-pi.output
index 7f3d6dc5..59a403d0 100644
--- a/packages/coln-compiler/test/golden/multi-pi.output
+++ b/packages/coln-compiler/test/golden/multi-pi.output
@@ -57,6 +57,10 @@ global entry named eq-multi-2-eq
 in mode: Conjunctive
 type: (x y : Int) -> Int
 value: eq-single-2
+global entry named eq-multi-2
+in mode: Conjunctive
+type: (x y : Int) -> Int
+value: x => y => 19
 global entry named eq-single-2-eq
 in mode: Conjunctive
 type: (x : Int) -> (y : Int) -> Int
@@ -127,19 +131,15 @@ global entry named eq-dep-tail-backward
 in mode: Conjunctive
 type: (F : Int -> Set) -> (f : (x : Int) -> (y : Int) -> (z : F y) -> F x) -> (x y : Int) -> (z : F y) -> F x
 value: F => f => f
-global entry named eq-multi-2
-in mode: Conjunctive
-type: (x y : Int) -> Int
-value: x => y => 19
 
 -- messages
 
 expected error[E0300]: expected type (x : Int) -> Int, but got type (x y : Int) -> Int
-83 | def eq-too-few : (x : Int) -> Int := eq-multi-2
-83 |                                      ^^^^^^^^^^
+81 | def eq-too-few : (x : Int) -> Int := eq-multi-2
+81 |                                      ^^^^^^^^^^
 types Int and (y : Int) -> Int are not equal 
 
 expected error[E0300]: expected type (x y z : Int) -> Int, but got type (x y : Int) -> Int
-86 | def eq-too-many : (x y z : Int) -> Int := eq-multi-2
-86 |                                           ^^^^^^^^^^
+84 | def eq-too-many : (x y z : Int) -> Int := eq-multi-2
+84 |                                           ^^^^^^^^^^
 types (z : Int) -> Int and Int are not equal 
diff --git a/packages/coln-compiler/test/golden/shadowing.coln b/packages/coln-compiler/test/golden/shadowing.coln
new file mode 100644
index 00000000..8a5e8686
--- /dev/null
+++ b/packages/coln-compiler/test/golden/shadowing.coln
@@ -0,0 +1,83 @@
+def parameter_shadowing (x : Int) (x : Int) : Int := x
+
+def lambda_shadowing (x : Int) : (^c y : Int) -> Int := x => x
+
+theory PiShadowing := (x : Int) -> (x : Int) -> Set
+
+theory FieldArgumentShadowing (x : Int) := sig
+  x : Int
+end
+
+def top : Int := 19
+
+def param_top_shadowing (top : Int) : Int := 34
+
+theory ParamTopTheory (top : Int) := sig
+end
+
+def Pair : Set := sig
+  x : Int
+  y : Int
+end
+
+realm PairRealm @ Pair
+  def root_arg (root : Int) : Int := 41
+
+  def realm_def : Int := 38
+  def def_arg (realm_def : Int) : Int := 23
+end
+
+theory Nasty := sig
+  B : Set
+  E : B -> Set
+  n : (b : B) -> (b : E b) -> Int
+end
+
+theory NastyParam (b : Int) := sig
+  E : Int -> Set
+  b : E b
+end
+
+## Forbidden examples
+
+attr expected-error "E0208"
+def Pair : Set := sig
+  x : String
+  y : String
+end
+
+attr expected-error "E0209"
+def ShadowField : Set := sig
+  x : Int
+  # TODO: the expected-error should go here
+  x : String
+end
+
+# Banish him to the
+realm ShadowRealm @ Pair
+end
+
+attr expected-error "E0208"
+realm ShadowRealm @ Pair
+end
+
+attr expected-error "E0208"
+realm ShadowRoot @ Pair
+  def root : Pair := struct
+    x := 1
+    y := 2
+  end
+end
+
+attr expected-error "E0208"
+realm ShadowRealmDefinition @ Pair
+  def thing : Pair := struct
+    x := 1
+    y := 2
+  end
+
+  def thing : Pair := struct
+    x := 3
+    y := 4
+  end
+end
diff --git a/packages/coln-compiler/test/golden/shadowing.output b/packages/coln-compiler/test/golden/shadowing.output
new file mode 100644
index 00000000..21cf664c
--- /dev/null
+++ b/packages/coln-compiler/test/golden/shadowing.output
@@ -0,0 +1,100 @@
+-- elaborated
+global entry named parameter_shadowing
+in mode: Conjunctive
+type: (x : Int) -> (x : Int) -> Int
+value: x => x => x
+global entry named lambda_shadowing
+in mode: Conjunctive
+type: (x : Int) -> (y : Int) -> Int
+value: x => x => x
+global entry named PiShadowing
+in mode: Conjunctive
+type: Theory
+value: (x : Int) -> (x : Int) -> Set
+global entry named FieldArgumentShadowing
+in mode: Conjunctive
+type: (x : Int) -> Theory
+value: x => sig
+  x : Int
+end
+global entry named top
+in mode: Conjunctive
+type: Int
+value: 19
+global entry named param_top_shadowing
+in mode: Conjunctive
+type: (top : Int) -> Int
+value: top => 34
+global entry named ParamTopTheory
+in mode: Conjunctive
+type: (top : Int) -> Theory
+value: top => sig
+end
+global entry named Pair
+in mode: Conjunctive
+type: Set
+value: sig
+  x : Int
+  y : Int
+end
+global entry named Nasty
+in mode: Conjunctive
+type: Theory
+value: sig
+  B : Set
+  E : B -> Set
+  n : (b : B) -> (b : E b) -> Int
+end
+global entry named NastyParam
+in mode: Conjunctive
+type: (b : Int) -> Theory
+value: b => sig
+  E : Int -> Set
+  b : E b
+end
+realm named PairRealm
+lowered: flatrealm
+  entities
+    table root := [a.x : Int, a.y : Int] primarykey []
+  end
+  definitions
+  end
+  rules
+    enforced root.foreignKey a.x a.y := root [a.x ↦ a.x, a.y ↦ a.y] ⊢ ⊤
+    monitored root.total := ⊤ ⊢ root []
+  end
+end
+realm named ShadowRealm
+lowered: flatrealm
+  entities
+    table root := [a.x : Int, a.y : Int] primarykey []
+  end
+  definitions
+  end
+  rules
+    enforced root.foreignKey a.x a.y := root [a.x ↦ a.x, a.y ↦ a.y] ⊢ ⊤
+    monitored root.total := ⊤ ⊢ root []
+  end
+end
+
+-- messages
+
+expected error[E0208]: duplicate definition of Pair
+44 | def Pair : Set := sig
+44 |     ^^^^
+
+expected error[E0209]: duplicate record field x
+53 |   x : String
+53 |   ^
+
+expected error[E0208]: duplicate definition of ShadowRealm
+61 | realm ShadowRealm @ Pair
+61 |       ^^^^^^^^^^^
+
+expected error[E0208]: duplicate definition of root
+66 |   def root : Pair := struct
+66 |       ^^^^
+
+expected error[E0208]: duplicate definition of thing
+79 |   def thing : Pair := struct
+79 |       ^^^^^
diff --git a/packages/coln-compiler/test/golden/tricky-clique-pair.coln b/packages/coln-compiler/test/golden/tricky-clique-pair.coln
index 0d3e4834..2dce1477 100644
--- a/packages/coln-compiler/test/golden/tricky-clique-pair.coln
+++ b/packages/coln-compiler/test/golden/tricky-clique-pair.coln
@@ -15,8 +15,8 @@ theory BipartiteOverConnection (^i G : BipartiteGraphOver) := sig
   blue-blue : G.blue -> G.blue -> Prop
   red/refl : (v : G.red) -> red-red v v
   blue/refl : (w : G.blue) -> blue-blue w w
-  red/trans : (v0 : G.red) -> (v1 : G.red) -> (w0 : G.blue) -> (w1 : G.blue) -> G.red-blue v0 w0 -> blue-blue w0 w1 -> G.blue-red w1 v1 -> red-red v0 v1
-  blue/trans : (w0 : G.blue) -> (w1 : G.blue) -> (v0 : G.red) -> (v1 : G.red) -> G.blue-red w0 v0 -> red-red v0 v1 -> G.red-blue v1 w1 -> blue-blue w0 w1
+  red/trans : (v0 v1 : G.red) -> (w0 w1 : G.blue) -> G.red-blue v0 w0 -> blue-blue w0 w1 -> G.blue-red w1 v1 -> red-red v0 v1
+  blue/trans : (w0 w1 : G.blue) -> (v0 v1 : G.red) -> G.blue-red w0 v0 -> red-red v0 v1 -> G.red-blue v1 w1 -> blue-blue w0 w1
 
   red-red-over : (v0 : G.red) -> G.red-over v0 -> (v1 : G.red) -> G.red-over v1 -> Prop
   blue-blue-over : (w0 : G.blue) -> G.blue-over w0 -> (w1 : G.blue) -> G.blue-over w1 -> Prop
@@ -27,8 +27,8 @@ theory BipartiteOverConnection (^i G : BipartiteGraphOver) := sig
   red-over/refl : (v : G.red) -> (x : G.red-over v) -> red-red-over v x v x
   blue-over/refl : (w : G.blue) -> (y : G.blue-over w) -> blue-blue-over w y w y
 
-  red/trans : (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> G.red-blue-over v0 x0 w0 y0 -> blue-blue-over w0 y0 w1 y1 -> G.blue-red-over w1 y1 v1 x1 -> red-red-over v0 x0 v1 x1
-  blue/trans : (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> G.blue-red-over w0 y0 v0 x0 -> red-red-over v0 x0 v1 x1 -> G.red-blue-over v1 x1 w1 y1 -> blue-blue-over w0 y0 w1 y1
+  red-over/trans : (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> G.red-blue-over v0 x0 w0 y0 -> blue-blue-over w0 y0 w1 y1 -> G.blue-red-over w1 y1 v1 x1 -> red-red-over v0 x0 v1 x1
+  blue-over/trans : (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> G.blue-red-over w0 y0 v0 x0 -> red-red-over v0 x0 v1 x1 -> G.red-blue-over v1 x1 w1 y1 -> blue-blue-over w0 y0 w1 y1
 end
 
 realm BipartiteGraphOverRealm @ BipartiteGraphOver
diff --git a/packages/coln-compiler/test/golden/tricky-clique-pair.output b/packages/coln-compiler/test/golden/tricky-clique-pair.output
index eb954390..e41387fd 100644
--- a/packages/coln-compiler/test/golden/tricky-clique-pair.output
+++ b/packages/coln-compiler/test/golden/tricky-clique-pair.output
@@ -20,16 +20,16 @@ value: G => sig
   blue-blue : G.blue -> G.blue -> Prop
   red/refl : (v : G.red) -> red-red v v
   blue/refl : (w : G.blue) -> blue-blue w w
-  red/trans : (v0 : G.red) -> (v1 : G.red) -> (w0 : G.blue) -> (w1 : G.blue) -> G.red-blue v0 w0 -> blue-blue w0 w1 -> G.blue-red w1 v1 -> red-red v0 v1
-  blue/trans : (w0 : G.blue) -> (w1 : G.blue) -> (v0 : G.red) -> (v1 : G.red) -> G.blue-red w0 v0 -> red-red v0 v1 -> G.red-blue v1 w1 -> blue-blue w0 w1
+  red/trans : (v0 v1 : G.red) -> (w0 w1 : G.blue) -> G.red-blue v0 w0 -> blue-blue w0 w1 -> G.blue-red w1 v1 -> red-red v0 v1
+  blue/trans : (w0 w1 : G.blue) -> (v0 v1 : G.red) -> G.blue-red w0 v0 -> red-red v0 v1 -> G.red-blue v1 w1 -> blue-blue w0 w1
   red-red-over : (v0 : G.red) -> G.red-over v0 -> (v1 : G.red) -> G.red-over v1 -> Prop
   blue-blue-over : (w0 : G.blue) -> G.blue-over w0 -> (w1 : G.blue) -> G.blue-over w1 -> Prop
   red-over/lift : (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> red-red v0 v1 -> red-red-over v0 x0 v1 x1
   blue-over/lift : (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> blue-blue w0 w1 -> blue-blue-over w0 y0 w1 y1
   red-over/refl : (v : G.red) -> (x : G.red-over v) -> red-red-over v x v x
   blue-over/refl : (w : G.blue) -> (y : G.blue-over w) -> blue-blue-over w y w y
-  red/trans : (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> G.red-blue-over v0 x0 w0 y0 -> blue-blue-over w0 y0 w1 y1 -> G.blue-red-over w1 y1 v1 x1 -> red-red-over v0 x0 v1 x1
-  blue/trans : (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> G.blue-red-over w0 y0 v0 x0 -> red-red-over v0 x0 v1 x1 -> G.red-blue-over v1 x1 w1 y1 -> blue-blue-over w0 y0 w1 y1
+  red-over/trans : (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> G.red-blue-over v0 x0 w0 y0 -> blue-blue-over w0 y0 w1 y1 -> G.blue-red-over w1 y1 v1 x1 -> red-red-over v0 x0 v1 x1
+  blue-over/trans : (w0 : G.blue) -> (y0 : G.blue-over w0) -> (w1 : G.blue) -> (y1 : G.blue-over w1) -> (v0 : G.red) -> (x0 : G.red-over v0) -> (v1 : G.red) -> (x1 : G.red-over v1) -> G.blue-red-over w0 y0 v0 x0 -> red-red-over v0 x0 v1 x1 -> G.red-blue-over v1 x1 w1 y1 -> blue-blue-over w0 y0 w1 y1
 end
 realm named BipartiteGraphOverRealm
 lowered: flatrealm
@@ -82,7 +82,43 @@ lowered: flatrealm
       a ↦ w,
       b ↦ w
     ]
-    chased init.connection-info.red/trans v0 x0 v1 x1 w0 y0 w1 y1 a c := v0 ∈ root.red [] ∧ x0 ∈ root.red-over [
+    chased init.connection-info.red/trans v0 v1 w0 w1 a c := v0 ∈ root.red [] ∧ v1 ∈ root.red [] ∧ w0 ∈ root.blue [] ∧ w1 ∈ root.blue [] ∧ a ∈ root.red-blue [
+      a ↦ v0,
+      b ↦ w0
+    ] ∧ init.connection-info.blue-blue [a ↦ w0, b ↦ w1] ∧ c ∈ root.blue-red [
+      a ↦ w1,
+      b ↦ v1
+    ] ⊢ init.connection-info.red-red [a ↦ v0, b ↦ v1]
+    chased init.connection-info.blue/trans w0 w1 v0 v1 a c := w0 ∈ root.blue [] ∧ w1 ∈ root.blue [] ∧ v0 ∈ root.red [] ∧ v1 ∈ root.red [] ∧ a ∈ root.blue-red [
+      a ↦ w0,
+      b ↦ v0
+    ] ∧ init.connection-info.red-red [a ↦ v0, b ↦ v1] ∧ c ∈ root.red-blue [
+      a ↦ v1,
+      b ↦ w1
+    ] ⊢ init.connection-info.blue-blue [a ↦ w0, b ↦ w1]
+    chased init.connection-info.red-over/lift v0 x0 v1 x1 := v0 ∈ root.red [] ∧ x0 ∈ root.red-over [
+      a ↦ v0
+    ] ∧ v1 ∈ root.red [] ∧ x1 ∈ root.red-over [
+      a ↦ v1
+    ] ∧ init.connection-info.red-red [
+      a ↦ v0,
+      b ↦ v1
+    ] ⊢ init.connection-info.red-red-over [v0 ↦ v0, a ↦ x0, v1 ↦ v1, b ↦ x1]
+    chased init.connection-info.blue-over/lift w0 y0 w1 y1 := w0 ∈ root.blue [] ∧ y0 ∈ root.blue-over [
+      a ↦ w0
+    ] ∧ w1 ∈ root.blue [] ∧ y1 ∈ root.blue-over [
+      a ↦ w1
+    ] ∧ init.connection-info.blue-blue [
+      a ↦ w0,
+      b ↦ w1
+    ] ⊢ init.connection-info.blue-blue-over [w0 ↦ w0, a ↦ y0, w1 ↦ w1, b ↦ y1]
+    chased init.connection-info.red-over/refl v x := v ∈ root.red [] ∧ x ∈ root.red-over [
+      a ↦ v
+    ] ⊢ init.connection-info.red-red-over [v0 ↦ v, a ↦ x, v1 ↦ v, b ↦ x]
+    chased init.connection-info.blue-over/refl w y := w ∈ root.blue [] ∧ y ∈ root.blue-over [
+      a ↦ w
+    ] ⊢ init.connection-info.blue-blue-over [w0 ↦ w, a ↦ y, w1 ↦ w, b ↦ y]
+    chased init.connection-info.red-over/trans v0 x0 v1 x1 w0 y0 w1 y1 a c := v0 ∈ root.red [] ∧ x0 ∈ root.red-over [
       a ↦ v0
     ] ∧ v1 ∈ root.red [] ∧ x1 ∈ root.red-over [
       a ↦ v1
@@ -106,7 +142,7 @@ lowered: flatrealm
       v ↦ v1,
       b ↦ x1
     ] ⊢ init.connection-info.red-red-over [v0 ↦ v0, a ↦ x0, v1 ↦ v1, b ↦ x1]
-    chased init.connection-info.blue/trans w0 y0 w1 y1 v0 x0 v1 x1 a c := w0 ∈ root.blue [] ∧ y0 ∈ root.blue-over [
+    chased init.connection-info.blue-over/trans w0 y0 w1 y1 v0 x0 v1 x1 a c := w0 ∈ root.blue [] ∧ y0 ∈ root.blue-over [
       a ↦ w0
     ] ∧ w1 ∈ root.blue [] ∧ y1 ∈ root.blue-over [
       a ↦ w1
@@ -130,28 +166,6 @@ lowered: flatrealm
       w ↦ w1,
       b ↦ y1
     ] ⊢ init.connection-info.blue-blue-over [w0 ↦ w0, a ↦ y0, w1 ↦ w1, b ↦ y1]
-    chased init.connection-info.red-over/lift v0 x0 v1 x1 := v0 ∈ root.red [] ∧ x0 ∈ root.red-over [
-      a ↦ v0
-    ] ∧ v1 ∈ root.red [] ∧ x1 ∈ root.red-over [
-      a ↦ v1
-    ] ∧ init.connection-info.red-red [
-      a ↦ v0,
-      b ↦ v1
-    ] ⊢ init.connection-info.red-red-over [v0 ↦ v0, a ↦ x0, v1 ↦ v1, b ↦ x1]
-    chased init.connection-info.blue-over/lift w0 y0 w1 y1 := w0 ∈ root.blue [] ∧ y0 ∈ root.blue-over [
-      a ↦ w0
-    ] ∧ w1 ∈ root.blue [] ∧ y1 ∈ root.blue-over [
-      a ↦ w1
-    ] ∧ init.connection-info.blue-blue [
-      a ↦ w0,
-      b ↦ w1
-    ] ⊢ init.connection-info.blue-blue-over [w0 ↦ w0, a ↦ y0, w1 ↦ w1, b ↦ y1]
-    chased init.connection-info.red-over/refl v x := v ∈ root.red [] ∧ x ∈ root.red-over [
-      a ↦ v
-    ] ⊢ init.connection-info.red-red-over [v0 ↦ v, a ↦ x, v1 ↦ v, b ↦ x]
-    chased init.connection-info.blue-over/refl w y := w ∈ root.blue [] ∧ y ∈ root.blue-over [
-      a ↦ w
-    ] ⊢ init.connection-info.blue-blue-over [w0 ↦ w, a ↦ y, w1 ↦ w, b ↦ y]
   end
   rules
     enforced root.red.foreignKey := root.red [] ⊢ ⊤