summaryrefslogtreecommitdiff
path: root/lib/ur/incl.urs
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ur/incl.urs')
-rw-r--r--lib/ur/incl.urs2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/ur/incl.urs b/lib/ur/incl.urs
index d0d78b36..2c77369f 100644
--- a/lib/ur/incl.urs
+++ b/lib/ur/incl.urs
@@ -9,7 +9,7 @@ val inv1 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K}
-> incl ([nm = t] ++ r) r'
-> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r))
-> f nm t r'
-val inv2 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K}
+val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K}
-> [[nm] ~ r] =>
incl ([nm = t] ++ r) r' -> incl r r'