diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,7 +1,7 @@
 cabal-version:      3.0
 
 name:               phino
-version:            0.0.0.33
+version:            0.0.0.34
 license:            MIT
 synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions
 description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -122,7 +122,9 @@
 meetCondition' (Y.Eq (Y.CmpAttr left) (Y.CmpAttr right)) subst _ = pure [subst | compareAttrs left right subst]
   where
     compareAttrs :: Attribute -> Attribute -> Subst -> Bool
-    compareAttrs (AtMeta left) (AtMeta right) _ = left == right
+    compareAttrs (AtMeta left) (AtMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of
+      (Just (MvAttribute left'), Just (MvAttribute right')) -> compareAttrs left' right' (Subst mp)
+      _ -> False
     compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup meta mp of
       Just (MvAttribute found) -> attr == found
       _ -> False
@@ -133,7 +135,9 @@
 meetCondition' (Y.Eq (Y.CmpExpr left) (Y.CmpExpr right)) subst _ = pure [subst | compareExprs left right subst]
   where
     compareExprs :: Expression -> Expression -> Subst -> Bool
-    compareExprs (ExMeta left) (ExMeta right) _ = left == right
+    compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of
+      (Just (MvExpression left' _), Just (MvExpression right' _)) -> compareExprs left' right' (Subst mp)
+      _ -> False
     compareExprs expr (ExMeta meta) (Subst mp) = case M.lookup meta mp of
       Just (MvExpression found _) -> expr == found
       _ -> False