diff options
Diffstat (limited to 'lib/ur/incl.urs')
-rw-r--r-- | lib/ur/incl.urs | 2 |
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' |