diff --git a/lojysamban.cabal b/lojysamban.cabal
--- a/lojysamban.cabal
+++ b/lojysamban.cabal
@@ -2,7 +2,7 @@
 cabal-version:		>= 1.6
 
 name:			lojysamban
-version:		0.0.8
+version:		0.0.8.1
 stability:		alpha
 author:			.iocikun.juj. <PAF01143@nifty.ne.jp>
 maintainer:		.iocikun.juj. <PAF01143@nifty.ne.jp>
diff --git a/src/LojysambanLib.hs b/src/LojysambanLib.hs
--- a/src/LojysambanLib.hs
+++ b/src/LojysambanLib.hs
@@ -8,7 +8,7 @@
 import LojbanTools
 import Prolog2 hiding (ask)
 import qualified Prolog2 as P
-import Language.Lojban.Parser hiding (LA, Brivla, KOhA, GOhA, NA, LerfuString, LI)
+import Language.Lojban.Parser hiding (LA, Brivla, KOhA, GOhA, NA, LerfuString, LI, Term)
 import qualified Language.Lojban.Parser as P
 import Data.Maybe
 import Data.Either
@@ -70,7 +70,7 @@
 --	show answer ++ "\n" ++
 --	show (q []) ++
 	result1 ++ if null answer2 then "" else
-		if length answer == 1 then answer2_1 else answer2
+		"\n.i " ++ if length answer == 1 then answer2_1 else answer2
 
 showAtom :: Atom -> String
 showAtom (LA n) = "la " ++ n
@@ -85,26 +85,20 @@
 	[] -> Nothing
 	((_, tv) : _) -> flip (<$>) tv $ \tv' -> case tv' of
 		Con v -> v
-		List vs -> ListA $ map (\(Con v) -> v) vs
+		List vs -> ListA $ map (\(Con v) -> v) $ vs
 		c@(Cons _ _) -> ListA $ map (\(Con v) -> v) $
 			(\(List vs) -> vs) $ getList c r
-{-
-		Cons v (List vs) -> ListA $
-			(\(Con v) -> v) (lookupValue v r) : map (\(Con v) -> v) vs
-		Cons v vs@(Var _ _) -> ListA $
-			(\(Con v) -> v) (lookupValue v r) : map (\(Con v) -> v)
-				((\(List l) -> l) $ lookupValue vs r)
--}
 		o -> error $ "maValue: " ++ show o ++ " r = " ++ show r
 
-getList :: (Eq sc, Eq s) => Term sc s -> Result sc s -> Term sc s
+getList :: (Show sc, Show s, Eq sc, Eq s) => Term sc s -> Result sc s -> Term sc s
 getList l@(List _) _ = l
 getList (Cons v var@(Var _ _)) r
-	| List vs <- lookupValue var r = List $
-		lookupValue v r : map (flip lookupValue r) vs
-	| c@(Cons _ _) <- lookupValue var r,
-		List vs <- getList c r = List $ lookupValue v r : vs
-getList _ _ = error "not implemented"
+--	| List vs <- var = List $
+--		v : vs
+	| c@(Cons _ _) <- var,
+		List vs <- getList c r = List $ v : vs
+getList (Cons v (List vs)) _ = List $ v : vs
+getList o _ = error $ "getList: not implemented" ++ show o
 
 isMA :: Term Scope Atom -> Bool
 isMA (Var [_] (KOhA "ma")) = True
diff --git a/src/NotUnif.hs b/src/NotUnif.hs
--- a/src/NotUnif.hs
+++ b/src/NotUnif.hs
@@ -7,8 +7,7 @@
 	checkNot,
 	deleteFromNot,
 	notUnification,
-	apply,
-	lookupValue,
+	applyIs
 ) where
 
 import Unif
diff --git a/src/Prolog2.hs b/src/Prolog2.hs
--- a/src/Prolog2.hs
+++ b/src/Prolog2.hs
@@ -6,8 +6,7 @@
 	Rule(..),
 	Term(..),
 	TwoD(..),
-	Result,
-	lookupValue
+	Result
 ) where
 
 import PrologTools
@@ -16,8 +15,7 @@
 ask :: (TwoD sc, Eq sc, Eq s) =>
 	sc -> Result sc s -> Fact sc s -> [Rule sc s] -> [Result sc s]
 ask sc ret q rs
-	| [Is, t, u] <- q sc =
-		maybeToList $ [([t], Just $ apply u ret)] `merge` ret
+	| is@(Is : _) <- q sc = maybeToList $ applyIs is ret
 	| otherwise = concat $ zipWith ar (iterate next $ down sc) rs
 	where
 	ar sc' r = askrule sc' ret q r rs
@@ -29,7 +27,7 @@
 	sc -> Result sc s -> Fact sc s -> Rule sc s -> [Rule sc s] -> [Result sc s]
 askrule sc ret q (Rule fact _ facts notFacts) rs
 --	| [Is, t, u] <- fact (next sc) = maybeToList $ [([t], Just u)] `merge` ret
-	| [Is, _, _] <- fact (next sc) = error "not implemented"
+	| [Is, _, _] <- fact (next sc) = error "askrule: not implemented"
 	| otherwise = filter (`checkAll` nots) ret'
 	where
 	ret' = foldl (\rets (sc', f) -> rets >>= \r' -> ask sc' r' f rs) r0 $
diff --git a/src/PrologTools.hs b/src/PrologTools.hs
--- a/src/PrologTools.hs
+++ b/src/PrologTools.hs
@@ -12,8 +12,7 @@
 	Rule(..),
 	notAsk,
 	checkAll,
-	apply,
-	lookupValue
+	applyIs
 ) where
 
 import NotUnif
diff --git a/src/Unif.hs b/src/Unif.hs
--- a/src/Unif.hs
+++ b/src/Unif.hs
@@ -1,40 +1,79 @@
 {-# LANGUAGE PatternGuards #-}
 
-module Unif (Term(..), Result, merge, unification, unify, apply, lookupValue) where
+module Unif (Result, Term(..), unification, merge, applyIs) where
 
 import Data.List(intersect, union)
+import Control.Applicative((<$>))
+import Control.Arrow(second)
 import Control.Monad(foldM)
 
-data Term sc s
-	= Con s | Var sc s | List [Term sc s] | Cons (Term sc s) (Term sc s)
-	| ApplyOp (s -> s -> s) (Term sc s) (Term sc s)
-	| Is
+type Result sc s = [Result1 sc s]
+type Result1 sc s = ([Term sc s], Maybe (Term sc s))
 
-instance (Show sc, Show s) => Show (Term sc s) where
-	show (Con x) = "Con " ++ show x
-	show (Var sc x) = "Var " ++ show sc ++ " " ++ show x
-	show (List ts) = "List " ++ show ts
-	show (Cons h t) = "Cons (" ++ show h ++ ") (" ++ show t ++ ")"
-	show (ApplyOp{}) = "ApplyOp _ _ _"
-	show Is = "Is"
+data Term sc s
+	= Var sc s | Con s | ApplyOp (s -> s -> s) (Term sc s) (Term sc s)
+	| Is | List [Term sc s] | Cons (Term sc s) (Term sc s)
 
 instance (Eq sc, Eq s) => Eq (Term sc s) where
-	Con x == Con y = x == y
 	Var sc x == Var sc' y = sc == sc' && x == y
+	Con x == Con y = x == y
+	ApplyOp{} == ApplyOp{} = error "can't compare applys"
+	Is == Is = True
 	List xs == List ys = xs == ys
 	Cons h t == Cons i u = h == i && t == u
-	ApplyOp{} == ApplyOp{} = error "can't compare applys"
 	_ == _ = False
 
-type Result sc s = [([Term sc s], Maybe (Term sc s))]
+instance (Show sc, Show s) => Show (Term sc s) where
+	show (Var sc x) = "(Var " ++ show sc ++ " " ++ show x ++ ")"
+	show (Con x) = "(Con " ++ show x ++ ")"
+	show (ApplyOp{}) = "(ApplyOp _ _ _)"
+	show Is = "Is"
+	show (List ts) = "(List " ++ show ts ++ ")"
+	show (Cons h t) = "(Cons (" ++ show h ++ ") (" ++ show t ++ "))"
 
+unification :: (Eq sc, Eq s) => [Term sc s] -> [Term sc s] -> Maybe (Result sc s)
+unification [] [] = Just []
+unification (t : ts) (u : us) = do
+	(_, ret) <- unify t u
+	merge ret =<< unification ts us
+unification _ _ = Nothing
+
+unify :: (Eq sc, Eq s) => Term sc s -> Term sc s -> Maybe (Term sc s, Result sc s)
+unify t u | t == u = Just (t, [])
+unify t@(Var _ _) u@(Var _ _) = Just (t, [([t, u], Nothing)])
+unify t@(Var _ _) u = Just (u, [([t], Just u)])
+unify t u@(Var _ _) = unify u t
+unify (Con _) (Con _) = Nothing
+unify (Con _) ApplyOp{} = error "unify Con{} ApplyOp{}: not implemented yet"
+unify t@ApplyOp{} u@(Con _) = unify u t
+unify (Con _) _ = Nothing
+unify _ (Con _) = Nothing
+unify ApplyOp{} ApplyOp{} = error "unify ApplyOp{} ApplyOP{}: not implemented yet"
+unify ApplyOp{} _ = Nothing
+unify _ ApplyOp{} = Nothing
+unify Is _ = Nothing
+unify _ Is = Nothing
+unify (List ts) (List us) = do
+	rs <- unification ts us
+	return (List $ map (`lookupValue` rs) ts, rs)
+unify (List []) Cons{} = Nothing
+unify (List (t : ts)) (Cons hd tl) = do
+	rs <- unification [t, List ts] [hd, tl]
+	return (List (lookupValue t rs : map (`lookupValue` rs) ts), rs)
+unify t@(Cons _ _) u@(List _) = unify u t
+unify (Cons h1 t1) (Cons h2 t2) = do
+	rs <- unification [h1, t1] [h2, t2]
+	return (Cons (lookupValue h1 rs) (lookupValue t1 rs), rs)
+
 merge :: (Eq sc, Eq s) => Result sc s -> Result sc s -> Maybe (Result sc s)
-merge ps qs = foldM (flip merge1) qs ps
+merge ps qs = simplifyResult <$> foldM (flip merge1) qs ps
 
-merge1 :: (Eq sc, Eq s) =>
-	([Term sc s], Maybe (Term sc s)) -> Result sc s -> Maybe (Result sc s)
+simplifyResult :: (Eq sc, Eq s) => Result sc s -> Result sc s
+simplifyResult rs = map (second $ fmap $ flip lookupValue rs) rs
+
+merge1 :: (Eq sc, Eq s) => Result1 sc s -> Result sc s -> Maybe (Result sc s)
 merge1 (ts, mv) r
-	| [(us, mv')] <- filter (isDefFor ts) r = do
+	| [(us, mv')] <- filter (isShare ts . fst) r = do
 		(vv, m) <- case (mv, mv') of
 			(Just v, Just v') -> do
 				(vv', m) <- unify v v'
@@ -42,13 +81,13 @@
 			(v, Nothing) -> return (v, [])
 			(_, v') -> return (v', [])
 		merge m $ (ts `union` us, vv) `add` notSames
-	| [] <- filter (isDefFor ts) r = return $ (ts, mv) `add` notSames
-	| [(us1, mv'1), (us2, mv'2)] <- filter (isDefFor ts) r = do
+	| [] <- filter (isShare ts . fst) r = return $ (ts, mv) `add` notSames
+	| [(us1, mv'1), (us2, mv'2)] <- filter (isShare ts . fst) r = do
 		ret1 <- fun (us1, mv'1) (ts, mv) notSames
 		fun (us2, mv'2) (ts `union` us1, mv) ret1
-	| err <- filter (isDefFor ts) r = error $ show $ length err
+	| err <- filter (isShare ts . fst) r = error $ show $ length err
 	where
-	notSames = filter (not . isDefFor ts) r
+	notSames = filter (not . isShare ts . fst) r
 	fun (_, mv') (tsss, mvvv) hoge = do
 		(vv, m) <- case (mvvv, mv') of
 			(Just v, Just v') -> do
@@ -58,56 +97,19 @@
 			(_, v') -> return (v', [])
 		merge m $ (tsss, vv) `add` hoge
 
-add :: (Eq sc, Eq s) =>
-	([Term sc s], Maybe (Term sc s)) -> Result sc s -> Result sc s
+add :: (Eq sc, Eq s) => Result1 sc s -> Result sc s -> Result sc s
 add (ts, v@(Just _)) rs = (foldr union ts sames, v) : notSames
 	where
 	sames = map fst $ filter ((== v) . snd) rs
 	notSames = filter ((/= v) . snd) rs
 add r1 rs = r1 : rs
 
-isDefFor :: (Eq sc, Eq s) => [Term sc s] -> ([Term sc s], Maybe (Term sc s)) -> Bool
-isDefFor ts (us, _) = not $ null $ ts `intersect` us
-
-unification :: (Eq sc, Eq s) => [Term sc s] -> [Term sc s] -> Maybe (Result sc s)
-unification = unifies
-
-unify :: (Eq sc, Eq s) => Term sc s -> Term sc s -> Maybe (Term sc s, Result sc s)
-unify t u | t == u = Just (t, [])
-unify (Con _) (Con _) = Nothing
-unify t@(Var _ _) u@(Var _ _) = Just (t, [([t, u], Nothing)])
-unify t@(Var _ _) u = Just (u, [([t], Just u)])
-unify t u@(Var _ _) = Just (t, [([u], Just t)])
-unify (List ts) (List us) = do
-	rs <- unification ts us
-	return (List $ map (`lookupValue` rs) ts, rs)
-unify (Cons h t) (List (u : us)) = do
-	rs <- unification [h, t] [u, List us]
-	return (Cons (lookupValue h rs) (lookupValue t rs), rs)
-unify (Cons _ _) (List []) = Nothing
-unify (Cons h1 t1) (Cons h2 t2) = do
-	rs <- unification [h1, t1] [h2, t2]
-	return (Cons (lookupValue h1 rs) (lookupValue t1 rs), rs)
-unify t u@(Cons _ _) = unify u t
-unify Is Is = Just (Is, [])
-unify Is _ = Nothing
-unify _ Is = Nothing
-unify (Cons _ _) (Con _) = Nothing -- error "Cons with Con"
-unify (Cons _ _) _ = error "Cons with _"
-unify (ApplyOp{}) (List _) = error "AppOp with List"
-unify (Con _) (List _) = Nothing -- error "Con with List"
-unify _ _ = error "not implemented"
-
-unifies :: (Eq sc, Eq s) => [Term sc s] -> [Term sc s] -> Maybe (Result sc s)
-unifies [] [] = Just []
-unifies (t : ts) (u : us) = do
-	(_, ret) <- unify t u
-	rets <- unifies ts us
-	merge ret rets
-unifies _ _ = Nothing
+isShare :: Eq a => [a] -> [a] -> Bool
+isShare = (.) (not . null) . intersect
 
 lookupValue :: (Eq sc, Eq s) => Term sc s -> Result sc s -> Term sc s
-lookupValue t rs =
+lookupValue t@(Con _) _ = t
+lookupValue t@(Var _ _) rs =
 	case f of
 		[] -> t
 		[(_, Nothing)] -> t
@@ -115,6 +117,14 @@
 		_ -> error "cannot occur"
 	where
 	f = filter ((t `elem`) . fst) rs
+lookupValue (List ts) rs = List $ map (`lookupValue` rs) ts
+lookupValue (Cons h t) rs = Cons (lookupValue h rs) (lookupValue t rs)
+lookupValue _ _ = error "lookupValue: not implemented"
+
+applyIs :: (Eq s, Eq sc) => [Term sc s] -> Result sc s -> Maybe (Result sc s)
+applyIs [Is, t@(Var _ _), u] rs = [([t], Just $ apply u rs)] `merge` rs
+applyIs (Is : _) _ = error "applyIs: Usage: Is [var] [val]"
+applyIs _ _ = error "cant apply Is"
 
 apply :: (Eq s, Eq sc) => Term sc s -> Result sc s -> Term sc s
 apply (ApplyOp op t u) rs