anchor.diff:  type private Solution = Map<QVar, Expr>
   exception NotMatched of string * Expr list
   
  -let private findVariableInList<'a> (key: Var) (col: 'a list) (conv: 'a -> Var): 'a option =
  -  metaVars.getMetaVarAmongGivenVarBindings key (col |> List.map (fun x -> conv x, x))
  +let private findVariableInList<'a> (key: QVar) (col: 'a list) (conv: 'a -> Var): 'a option =
  +  metaVars.getMetaVarAmongGivenVarBindings (key.var) (col |> List.map (fun x -> conv x, x))
       |> Option.map snd
   
  -let private variableMapGet<'a> (key: Var) (map: Map<QVar, 'a>): 'a option = 
  -  let res = findVariableInList key (Map.toList map) (fun (QVar(v), _) -> v) |> Option.map snd
  +let private variableMapGet<'a> (key: QVar) (map: Map<QVar, 'a>): 'a option = 
  +  let res = findVariableInList key (Map.toList map) (fun (qv, _) -> qv.var) |> Option.map snd
     match res with
     | Some v -> res
  -  | None   -> map.TryFind (QVar key)
  -
  -let private solutionsGet (key: Var) (solutions: Solution): Expr option = 
  +  | None   -> map.TryFind (key) 
  +
  +let private solutionsGet (key: QVar) (solutions: Solution): Expr option = 
     variableMapGet key solutions
   
   let rec private substVars (solutions: Solution) (e: Expr): Expr =
  -  e.Substitute(fun v -> solutions |> solutionsGet v)
  +  e.Substitute(fun v -> solutions |> solutionsGet (TypedVar v)) // TODO
   
   let rec private substAndReduce (solutions: Solution) (betaVars: Set<QVar>) (e: Expr) = 
     match e with
  -  | AppN(Patterns.Var(v), args) when findVariableInList v (Set.toList betaVars) (fun x -> x.var) |> Option.isSome ->
  -    match solutionsGet v solutions with
  +  | AppN(Patterns.Var(v), args) when findVariableInList (UntypedVar v) (Set.toList betaVars) (fun x -> x.var) |> Option.isSome -> // TODO
  +    match solutionsGet (UntypedVar v) solutions with // TODO
       | Some(LambdaN(inputs, body)) -> 
  -      let inlinedBody = substVars (List.zip (inputs |> List.map QVar) args |> Map.ofList) body
  +      let inlinedBody = substVars (List.zip (inputs |> List.map TypedVar) args |> Map.ofList) body // TODO
         substAndReduce solutions betaVars inlinedBody
       | Some(e2) -> Expr.Applications(e2, List.map (fun x -> [substAndReduce solutions betaVars x]) args)
       | None -> failwithf "There is no corresponding value in the solutions %A for the hoVar %A" solutions v
     | _ ->
       match e with
  -    | Patterns.Var(v) -> solutions |> solutionsGet v |> Option.fold (fun _ x -> x) e
  +    | Patterns.Var(v) -> solutions |> solutionsGet (TypedVar v) |> Option.fold (fun _ x -> x) e // TODO
       | LambdaN(inputs, body) -> LambdaN(inputs, substAndReduce solutions betaVars body)
       | ExprShape.ShapeCombination(op, args) -> ExprShape.RebuildShapeCombination(op, args |> List.map (substAndReduce solutions betaVars))
       | _ -> failwithf "substAndReduce doesn't handle %A" e
   
  -let private recordSolution (key: Var, value: Expr) (solutions: Solution): Solution = 
  +let private recordSolution (key: QVar, value: Expr) (solutions: Solution): Solution = 
     match solutionsGet key solutions with
     | Some value2 ->
       if alphaEquals value value2 then 
  
positive.code:       // Record the solution of hoVar  
        let vinsts = recordSolution (hoVar, lambdaTerm) solutions  
    
        vinsts, hoVars.Add qhoVar  
  
  let rec private termPartialMatch (env: Map<QVar,QVar>) ((solutions: Solution, hoMatches: HoMatch list) as acc) (pat: Expr) (term: Expr): Solution * HoMatch list =  
    match (pat, term) with
    | Patterns.Var patv, _ ->
      match variableMapGet patv env with
      | Some v2 ->
        if term = Expr.Var(v2.var) then
          acc
        else 
          raise ( NotMatched("Unification problem", [pat; term; Expr.Var(v2.var)]) )
      | None ->
        let newSolutions = recordSolution (patv, term) solutions
        newSolutions, hoMatches
    | (Patterns.Call(None, op, pats), Patterns.Call(None, oe, exprs)) when (List.length pats) = (List.length exprs) && op.Name = oe.Name && op.Module.Name = oe.Module.Name ->
      (acc,pats,exprs) |||> List.fold2 (termPartialMatch env)
  
negative.code:     resultVar |> Option.map (fun v -> givenVarBindings |> List.find(fun (v2, _) -> v2.Name = v.Name))
    let isAMetaVar (var: Var): bool = 
      getMetaVarAmongGivenVarBindings var (allMetaVars @ allGenericMetaVars |> List.map (fun v -> getExprVar(v), 1)) |> Option.isSome
    let getQMetaVar (var: Var): QVar option =
      let untypedVar = 
        allGenericMetaVars 
        |> List.tryFind (fun e -> (getExprVar e).Name = var.Name)
        |> Option.map (fun e -> UntypedVar (getExprVar e))
      match untypedVar with
      | Some v -> untypedVar
      | None   ->
        allMetaVars 
        |> List.map getExprVar
        |> List.tryFind (fun v -> v = var)
        |> Option.map (fun v -> TypedVar v)
  
  (*
  // Inspired by: https://github.com/jrh13/hol-light/blob/master/nets.ml
  