diff --git a/parsing/Pretty.ml b/parsing/Pretty.ml
index 7a8ca03f..1cd305da 100644
--- a/parsing/Pretty.ml
+++ b/parsing/Pretty.ml
@@ -293,15 +293,15 @@ let string_of_stages (st:stagedSpec) : string =
   | Require (p, h) ->
     Format.asprintf "req %s" (string_of_state (p, h))
   | HigherOrder (pi, h, (f, args), ret) ->
-    Format.asprintf "%s /\\ %s$(%s, %s); " (string_of_state (pi, h)) f (string_of_args args) (string_of_term ret)
+    Format.asprintf "%s(%s, %s, %s)" f (string_of_state (pi, h)) (string_of_args args) (string_of_term ret)
   | NormalReturn (pi, heap, ret) ->
     Format.asprintf "Norm(%s, %s)" (string_of_state (pi, heap))  (string_of_term ret)
   | RaisingEff (pi, heap, (name, args), ret) ->
     Format.asprintf "%s(%s, %s, %s)" name (string_of_state (pi, heap)) (string_of_args args) (string_of_term ret)
   | Exists vs ->
     Format.asprintf "ex %s" (String.concat " " vs)
-  | Pred {name; vars} ->
-    Format.asprintf "%s(%s)" name (String.concat " " vars)
+  (* | IndPred {name; args} -> *)
+    (* Format.asprintf "%s(%s)" name (String.concat " " (List.map string_of_term args)) *)
 
 let string_of_spec (spec:spec) :string =
   match spec with
@@ -317,6 +317,9 @@ let rec string_of_spec_list (specs:spec list) : string =
   | [x] -> string_of_spec x 
   | x :: xs -> string_of_spec x ^ " \\/ " ^ string_of_spec_list xs 
 
+let string_of_pred ({ p_name; p_params; p_body } : pred_def) : string =
+  Format.asprintf "%s(%s) :- %s" p_name (String.concat "," p_params) (string_of_spec_list p_body)
+
 let string_of_inclusion (lhs:spec list) (rhs:spec list) :string = 
   string_of_spec_list lhs ^" |- " ^string_of_spec_list rhs 
   ;;
@@ -524,8 +527,8 @@ let normalise_stagedSpec (acc:normalisedStagedSpec) (stagedSpec:stagedSpec) : no
   | HigherOrder (pi, heap, ins, ret') ->
     let v = verifier_getAfreeVar ~from:"n" () in
     (effectStages@[(existential, req, mergeState ens (pi, heap), ins , ret')], freshNormStageVar v)
-  | Pred {name; _} ->
-    failwith (Format.asprintf "cannot normalise predicate %s" name)
+  (* | IndPred {name; _} -> *)
+    (* failwith (Format.asprintf "cannot normalise predicate %s" name) *)
 
 let rec normalise_spec_ (acc:normalisedStagedSpec) (spec:spec) : normalisedStagedSpec = 
   match spec with 
@@ -757,7 +760,7 @@ let%expect_test "normalise spec" =
   ==>
   req 1=1; E(x->1 /\ 1=1, [3], ()); req emp; Norm(y->2, ())
 
-  Norm(x->1, ()); emp /\ f$([3], ()); ; Norm(y->2, ())
+  Norm(x->1, ()); f(emp, [3], ()); Norm(y->2, ())
   ==>
   req emp; f(x->1, [3], ()); req emp; Norm(y->2, ())
 |}]
diff --git a/parsing/entail.ml b/parsing/entail.ml
index fb8d0cdb..145b4820 100644
--- a/parsing/entail.ml
+++ b/parsing/entail.ml
@@ -78,6 +78,50 @@ let string_of_instantiations kvs =
   List.map (fun (k, v) -> Format.asprintf "%s := %s" k v) kvs
   |> String.concat ", " |> Format.asprintf "[%s]"
 
+(** a lemma is a formula such as f$(a, r) |= c(a, r) *)
+type lemma = {
+  l_name : string;
+  l_vars : string list;
+  l_left : stagedSpec;
+  l_right : spec;
+}
+
+let instantiate_lemma : lemma -> term list -> lemma =
+ fun lem args ->
+  let bs = List.map2 (fun a b -> (a, b)) lem.l_vars args in
+  {
+    lem with
+    l_left = (Forward_rules.instantiateStages bs) lem.l_left;
+    l_right = List.map (Forward_rules.instantiateStages bs) lem.l_right;
+  }
+
+let instantiate_pred : pred_def -> term list -> pred_def =
+ fun pred args ->
+  let bs = List.map2 (fun a b -> (a, b)) pred.p_params args in
+  {
+    pred with
+    p_body =
+      List.map
+        (fun b -> List.map (Forward_rules.instantiateStages bs) b)
+        pred.p_body;
+  }
+
+(** single application *)
+let apply_lemma : lemma -> spec -> spec =
+ fun lem sp ->
+  let tr s =
+    (* for now, lemmas are only applied from left to right, and the left side must be a predicate *)
+    match (s, lem.l_left) with
+    | Exists _, _ | Require (_, _), _ | NormalReturn _, _ | RaisingEff _, _ ->
+      [s]
+    | ( HigherOrder (_p, _h, (name, args), _r),
+        HigherOrder (_, _, (name1, _args1), _) )
+      when String.equal name name1 ->
+      (instantiate_lemma lem args).l_right
+    | HigherOrder _, _ -> [s]
+  in
+  List.concat_map tr sp
+
 let conj xs =
   match xs with
   | [] -> True
@@ -490,15 +534,22 @@ let rec check_staged_subsumption_ :
 (* let debug = false *)
 let ( let@ ) f x = f x
 
+(** Given two heap formulae, matches points-to predicates
+  may backtrack if the locations are quantified.
+  returns (by invoking the continuation) when matching is complete (when right is empty).
+
+  id: human-readable name
+  vs: quantified variables
+  k: continuation
+*)
 let rec check_qf2 :
     string ->
-    pi ->
     string list ->
     state ->
     state ->
     (pi * pi -> 'a Res.pf) ->
     'a Res.pf =
- fun id eqs vs ante conseq k ->
+ fun id vs ante conseq k ->
   let a = Heap.normalize ante in
   let c = Heap.normalize conseq in
   match (a, c) with
@@ -536,7 +587,7 @@ let rec check_qf2 :
               let _unifier = Atomic (EQ, Var fl, Var fr) in
               let triv = Atomic (EQ, v, v1) in
               (* matching ptr values are added as an eq to the right side, since we don't have a term := term substitution function *)
-              check_qf2 id True vs (conj [p1], h1') (conj [p2; triv], h2') k)
+              check_qf2 id vs (conj [p1], h1') (conj [p2; triv], h2') k)
         in
         begin
           match r1 with
@@ -557,7 +608,7 @@ let rec check_qf2 :
         (* let  *)
         (* And (p1, Atomic (EQ, v, v1)) *)
         (* match *)
-        check_qf2 (* (SepConj (k, PointsTo (x, v))) *) id eqs vs
+        check_qf2 (* (SepConj (k, PointsTo (x, v))) *) id vs
           (conj [p1], h1')
           (conj [p2], h2')
           k
@@ -583,6 +634,17 @@ let rec check_qf2 :
     | None -> failwith (Format.asprintf "could not split LHS, bug?")
   end
 
+(** recurses down a normalised staged spec, matching stages,
+   translating away heap predicates to build a pure formula,
+   then proving it at the end.
+
+   quantifiers are left to z3 to instantiate because they are shared across stages,
+   so instantiation has to be delayed until we know the entire formula.
+   
+   i: index of stage
+   all_vars: quantified variables
+   so_far: conjuncts of the formula we're building, together with human-readable form
+*)
 let rec check_staged_subsumption2 :
     int ->
     string list ->
@@ -598,12 +660,11 @@ let rec check_staged_subsumption2 :
 
     let triv = Atomic (EQ, r1, r2) in
 
-    (* let _ = *)
     let@ pre_l, pre_r =
-      check_qf2 (Format.asprintf "pre%d" i) True all_vars (p2, h2) (p1, h1)
+      check_qf2 (Format.asprintf "pre%d" i) all_vars (p2, h2) (p1, h1)
     in
     let@ post_l, post_r =
-      check_qf2 (Format.asprintf "post%d" i) True all_vars (qp1, qh1) (qp2, qh2)
+      check_qf2 (Format.asprintf "post%d" i) all_vars (qp1, qh1) (qp2, qh2)
     in
     let fml =
       [
@@ -638,11 +699,9 @@ let rec check_staged_subsumption2 :
     in
 
     (* contra *)
-    let@ pre_l, pre_r = check_qf2 "pren" True all_vars (p2, h2) (p1, h1) in
+    let@ pre_l, pre_r = check_qf2 "pren" all_vars (p2, h2) (p1, h1) in
     (* cov *)
-    let@ post_l, post_r =
-      check_qf2 "postn" True all_vars (qp1, qh1) (qp2, qh2)
-    in
+    let@ post_l, post_r = check_qf2 "postn" all_vars (qp1, qh1) (qp2, qh2) in
     let fml =
       [
         ( Format.asprintf "norm res eq: %s = %s" (string_of_term r1)
@@ -683,20 +742,35 @@ let rec check_staged_subsumption2 :
     else Error (rule ~name:"subsumption-base" ~success:false "fail")
   | _ -> Error (rule ~name:"subsumption-stage" ~success:false "unequal length")
 
-let check_staged_subsumption : spec -> spec -> state Res.pf =
- fun n1 n2 ->
-  (* replace quantified variables on the left side with fresh variables *)
-  let es1, ns1 =
-    let norm = normalise_spec n1 in
-    norm
-    (* let vars = Forward_rules.getExistientalVar norm in
-       let vars_fresh =
-         List.map (fun v -> (v, Var (verifier_getAfreeVar ()))) vars
-       in
-       let es1, (_, pre, post, ret) = instantiate_existentials vars_fresh norm in
-       ( List.map (fun (_, pre, post, eff, ret) -> ([], pre, post, eff, ret)) es1,
-         ([], pre, post, ret) ) *)
+(** f;a;e \/ b and a == c \/ d
+  => f;(c \/ d);e \/ b
+  => f;c;e \/ f;d;e \/ b *)
+let unfold_predicate : pred_def -> disj_spec -> disj_spec =
+ fun pred ds ->
+  let rec loop prefix already s =
+    match s with
+    | [] -> List.map List.rev prefix
+    | HigherOrder (_p, _h, (name, args), _r) :: s1
+      when String.equal name pred.p_name && not (List.mem name already) ->
+      (* unfold *)
+      let pred1 = instantiate_pred pred args in
+      let pref : disj_spec =
+        List.concat_map (fun p -> List.map (fun b -> b @ p) pred1.p_body) prefix
+      in
+      loop pref already s1
+    | c :: s1 ->
+      let pref = List.map (fun p -> c :: p) prefix in
+      loop pref already s1
   in
+  List.concat_map (fun s -> loop [] [] s) ds
+
+let check_staged_subsumption : lemma list -> spec -> spec -> state Res.pf =
+ fun lems n1 n2 ->
+  (* apply lemmas once *)
+  let n1 = List.fold_right apply_lemma lems n1 in
+  let n2 = List.fold_right apply_lemma lems n2 in
+  (* proceed *)
+  let es1, ns1 = normalise_spec n1 in
   let es2, ns2 = normalise_spec n2 in
   (* check_staged_subsumption_ (es1, ns1) (es2, ns2) *)
   check_staged_subsumption2 0
@@ -704,10 +778,26 @@ let check_staged_subsumption : spec -> spec -> state Res.pf =
     @ Forward_rules.getExistientalVar (es2, ns2))
     [] (es1, ns1) (es2, ns2)
 
+(**
+  Subsumption between disjunctive specs.
+  S1 \/ S2 |= S3 \/ S4
+*)
+let subsumes_disj :
+    lemma list -> pred_def list -> disj_spec -> disj_spec -> state list Res.pf =
+ fun lems preds ds1 ds2 ->
+  (* unfold all predicates once *)
+  let ds1 = List.fold_right unfold_predicate preds ds1 in
+  let ds2 = List.fold_right unfold_predicate preds ds2 in
+  (* proceed *)
+  Res.all ~may_elide:true ~name:"subsumes-disj-lhs-all" ~to_s:string_of_spec ds1
+    (fun s1 ->
+      Res.any ~may_elide:true ~name:"subsumes-disj-rhs-any" ~to_s:string_of_spec
+        ds2 (fun s2 -> check_staged_subsumption lems s1 s2))
+
 let%expect_test "staged subsumption" =
   verifier_counter_reset ();
   let test name l r =
-    let res = check_staged_subsumption l r in
+    let res = check_staged_subsumption [] l r in
     Format.printf "\n--- %s\n%s\n%s\n%s%s@." name (string_of_spec l)
       (match res with Ok _ -> "|--" | Error _ -> "|-/-")
       (string_of_spec r)
@@ -813,16 +903,6 @@ let%expect_test "staged subsumption" =
     ==> emp
     │[subsumption-stage] E(x->a+1, [], r); req x->a; Norm(x->a+1, r) |= E(x->a+1, [], r); req x->1; Norm(x->1, r) |}]
 
-(**
-  Subsumption between disjunctive specs.
-  S1 \/ S2 |= S3 \/ S4
-*)
-let subsumes_disj ds1 ds2 =
-  Res.all ~may_elide:true ~name:"subsumes-disj-lhs-all" ~to_s:string_of_spec ds1
-    (fun s1 ->
-      Res.any ~may_elide:true ~name:"subsumes-disj-rhs-any" ~to_s:string_of_spec
-        ds2 (fun s2 -> check_staged_subsumption s1 s2))
-
 module Normalize = struct
   let rec sl_dom (h : kappa) =
     match h with
diff --git a/parsing/forward_rules.ml b/parsing/forward_rules.ml
index b90c1d62..bae8049d 100644
--- a/parsing/forward_rules.ml
+++ b/parsing/forward_rules.ml
@@ -19,12 +19,13 @@ let concatenateSpecsWithSpec (current:spec list) (event:spec list) :  spec list
   let temp  = List.map (fun a -> concatenateSpecsWithEvent current a) event in 
   List.flatten temp
 
-let rec retriveNormalStage (spec:spec) : (pi * kappa * term) = 
+let rec retrieve_return_value (spec:spec) : term = 
   match spec with 
-  | [] -> failwith "retriveNormalStage empty spec"
-  | [NormalReturn (pN, hN, retN)] 
-  | [RaisingEff(pN, hN,_ ,  retN)] -> (pN, hN, retN)
-  | _ :: xs -> retriveNormalStage xs 
+  | [] -> failwith "retrieve_return_value empty spec"
+  | [HigherOrder (_, _, _, retN)] 
+  | [NormalReturn (_, _, retN)] 
+  | [RaisingEff(_, _, _, retN)] -> retN
+  | _ :: xs -> retrieve_return_value xs 
 
 let rec retriveSpecFromEnv (fname: string) (env:meth_def list) : (string list * spec list) option = 
   match env with 
@@ -109,6 +110,9 @@ let instantiateStages (bindings:((string * core_value) list))  (stagedSpec:stage
     RaisingEff (instantiatePure bindings pi, instantiateHeap bindings  kappa, (label, 
     List.map (fun bt -> instantiateTerms bindings bt) basic_t_list
     ), instantiateTerms bindings ret) 
+  (* | Pred {name; args}  ->  *)
+    (* Pred {name; args = List.map (instantiateTerms bindings) args} *)
+
 
 
 let instantiateSpec (bindings:((string * core_value) list)) (sepc:spec) : spec = 
@@ -258,7 +262,7 @@ and infer_of_expression (env:meth_def list) (current:spec list) (expr:core_lang)
     let phi1 = infer_of_expression env current expr1 in 
     List.flatten (List.map (fun spec -> 
       (*print_endline (string_of_spec(spec)); *)
-      let (_, _, retN) = retriveNormalStage spec in 
+      let retN = retrieve_return_value spec in 
       match retN with 
       | UNIT -> infer_of_expression env [spec] expr2
       (*| Var freshV -> 
@@ -370,17 +374,20 @@ and infer_of_expression (env:meth_def list) (current:spec list) (expr:core_lang)
       | _ -> failwith ("wrong aruguments of - " )
 
     else 
-    (match retriveSpecFromEnv fname env with 
-    | None -> failwith ("no implemnetation of " ^ fname )
-    | Some  (formalArgs, spec_of_fname) -> 
-      (*print_endline (string_of_spec_list spec_of_fname);*)
-      let spec_of_fname =renamingexistientalVar spec_of_fname in 
-      (*print_endline ("====\n"^ string_of_spec_list spec_of_fname);*)
-
-      let bindings = bindFormalNActual (formalArgs) (actualArgs) in 
-      let instantiatedSpec =  instantiateSpecList bindings spec_of_fname in 
-      concatenateSpecsWithSpec current instantiatedSpec  
-    )
+    let spec_of_fname =
+      match retriveSpecFromEnv fname env with 
+      | None ->
+        let ret = verifier_getAfreeVar () in
+        [[Exists [ret]; HigherOrder (True, EmptyHeap, (fname, actualArgs), Var ret)]]
+      | Some (formalArgs, spec_of_fname) -> 
+        (*print_endline (string_of_spec_list spec_of_fname);*)
+        let spec = renamingexistientalVar spec_of_fname in
+        let bindings = bindFormalNActual (formalArgs) (actualArgs) in 
+        let instantiatedSpec =  instantiateSpecList bindings spec in 
+        instantiatedSpec
+        (*print_endline ("====\n"^ string_of_spec_list spec_of_fname);*)
+    in
+    concatenateSpecsWithSpec current spec_of_fname  
 
 (* 
 ex i; Norm(i->0, i); ex f4; 
@@ -400,8 +407,8 @@ Norm(i->f5+1, ()); Norm(emp, f4)
 
 
   | CIfELse (v, expr2, expr3) -> 
-    let eventThen = NormalReturn (Atomic(GT, v, Num 0), EmptyHeap, UNIT) in 
-    let eventElse = NormalReturn (Atomic(LT, v, Num 0), EmptyHeap, UNIT) in 
+    let eventThen = NormalReturn (Atomic(EQ, v, Num 0), EmptyHeap, UNIT) in 
+    let eventElse = NormalReturn (Not(Atomic(EQ, v, Num 0)), EmptyHeap, UNIT) in 
     let currentThen = concatenateSpecsWithEvent current [eventThen] in 
     let currentElse = concatenateSpecsWithEvent current [eventElse] in 
     (infer_of_expression env currentThen expr2) @ 
diff --git a/parsing/hiplib.ml b/parsing/hiplib.ml
index 7d129ee9..2b2c4e75 100644
--- a/parsing/hiplib.ml
+++ b/parsing/hiplib.ml
@@ -582,6 +582,10 @@ let rec transformation (env:string list) (expr:expression) : core_lang =
   match expr.pexp_desc with 
   | Pexp_ident {txt=Lident i; _} ->
     CValue (Var i)
+  | Pexp_construct ({txt=Lident "true"; _}, None) ->
+    CValue (Num 0)
+  | Pexp_construct ({txt=Lident "false"; _}, None) ->
+    CValue (Num 1)
   | Pexp_construct ({txt=Lident "()"; _}, None) ->
     CValue (UNIT)
   | Pexp_constant c ->
@@ -744,11 +748,11 @@ let transform_str env (s : structure_item) =
     | Pexp_fun (_, _, _, tlbody) ->
       let spec =
         match function_spec tlbody with
-        | None -> [] 
-        | Some spec -> [spec]
+        | None -> failwith (Format.asprintf "%s has no spec, not yet supported" fn_name)
+        | Some spec -> spec
       in
       let formals, body = collect_param_names fn in
-      let e = transformation env body in
+      let e = transformation (fn_name :: formals @ env) body in
       `Meth (fn_name, formals, spec, e)
     | _ ->
       failwith (Format.asprintf "not a function binding: %a" Pprintast.expression fn)
@@ -1009,7 +1013,7 @@ let rec entailmentchecking (lhs:normalisedStagedSpec list) (rhs:normalisedStaged
 let run_string_ incremental line =
   let progs = Parser.implementation Lexer.token (Lexing.from_string line) in
   let prog = transform_strs progs in
-  (* print_endline (string_of_program (_effs, methods)); *)
+  (* print_endline (string_of_program prog); *)
   List.iter (fun (_name, _params, given_spec, body) ->
     (* this is done so tests are independent.
        each function is analyzed in isolation so this is safe. *)
@@ -1023,7 +1027,7 @@ let run_string_ incremental line =
       let time_stamp_afterNormal = Sys.time() in
       (* let res = entailmentchecking inferred_spec_n given_spec_n in *)
       let res =
-        match Entail.subsumes_disj inferred_spec given_spec with
+        match Entail.subsumes_disj [] [] inferred_spec given_spec with
         | Ok _ -> true
         | Error _ -> false
       in 
diff --git a/parsing/hiptypes.ml b/parsing/hiptypes.ml
index 898b2b78..dd7f478d 100644
--- a/parsing/hiptypes.ml
+++ b/parsing/hiptypes.ml
@@ -40,10 +40,11 @@ type stagedSpec =
       (* H /\ P /\ res=term *)
       | NormalReturn of (pi * kappa * term)
       (* higher-order functions: H /\ P /\ f$(...args, term) *)
+      (* this constructor is also used for inductive predicate applications *)
       | HigherOrder of (pi * kappa * instant * term)
       (* effects: H /\ P /\ E(...args, v), term is always a placeholder variable *)
       | RaisingEff of (pi * kappa * instant * term)
-      | Pred of { name : string; vars: string list }
+      (* | IndPred of { name : string; args: term list } *)
 
 (* type spec = (pi * linearStagedSpec) list  *)
 type spec = stagedSpec list
@@ -85,7 +86,7 @@ type meth_def = string * (string list) * (spec list) * core_lang
 
 type pred_def = {
   p_name: string;
-  p_vars: string;
+  p_params: string list;
   p_body: disj_spec;
 }
 
diff --git a/parsing/parser.mly b/parsing/parser.mly
index ec714115..d96da2be 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -2635,6 +2635,22 @@ stagedSpec1 :
       let init, last = split a in
       RaisingEff (p, h, (constr, init), last)
   }
+  | constr=LIDENT args=delimited(LPAREN, separated_nonempty_list(COMMA, effect_trace_value), RPAREN)
+  {
+    (* INFIXOP0 *)
+    (* we dn't check if the infix op is a dollar *)
+    (* why is basic stuff like this not available *)
+    let rec split xs =
+      match xs with
+      | [] -> failwith "split"
+      | [x] -> ([], x)
+      | x :: xs ->
+        let init, last = split xs in
+        (x :: init, last)
+    in
+    let init, last = split args in
+    HigherOrder (True, EmptyHeap, (constr, init), last)
+  }
 
 heapkappa:
 | EMP { EmptyHeap }
@@ -2647,7 +2663,7 @@ effect_spec:
 | stages=separated_nonempty_list(SEMI, stagedSpec1) { stages }
 
 fn_contract:
-  | LSPECCOMMENT spec = effect_spec RSPECCOMMENT
+  | LSPECCOMMENT spec=separated_nonempty_list(DISJUNCTION, effect_spec) RSPECCOMMENT
     // post_condition = list_of_post_condition 
     {Some spec}
 // Some ([], spec)
diff --git a/parsing/parsetree.ml b/parsing/parsetree.ml
index 47ee5ce8..67a5f317 100644
--- a/parsing/parsetree.ml
+++ b/parsing/parsetree.ml
@@ -265,7 +265,7 @@ and expression =
      pexp_loc: Location.t;
      pexp_loc_stack: location_stack;
      pexp_attributes: attributes; (* ... [@id1] [@id2] *)
-     pexp_effectspec: spec option;
+     pexp_effectspec: disj_spec option;
      (* (spec * spec list) option; *)
     }
 
diff --git a/src/programs.t/check.py b/src/programs.t/check.py
index f506394b..f9a7f894 100755
--- a/src/programs.t/check.py
+++ b/src/programs.t/check.py
@@ -3,15 +3,17 @@
 import sys
 first = True
 a = ''
+failed = False
 for l in sys.stdin:
   if first:
     a = l.rstrip()
   else:
-    if 'true' in a and 'true' not in l:
+    if ('true' in a and 'true' not in l) or ('false' in a and 'false' not in l):
+      if not failed:
+        print('TESTS FAILED')
+        failed = True
       print(a)
-      print(l)
-    elif 'true' in a and 'true' not in l:
-      print(a)
-      print(l)
   first = not first
-  
+
+if not failed:
+  print('ALL OK!')
\ No newline at end of file
diff --git a/src/programs.t/inductive.ml b/src/programs.t/inductive.ml
new file mode 100644
index 00000000..72952c20
--- /dev/null
+++ b/src/programs.t/inductive.ml
@@ -0,0 +1,7 @@
+let rec applyN f n x
+(*@ applyN(f, n, x, r); Norm(emp, r) @*)
+=
+  if n = 0 then x
+  else
+    let r = f x in
+    applyN f (n - 1) r
diff --git a/src/programs.t/run.t b/src/programs.t/run.t
index 202dc2da..74e9534b 100644
--- a/src/programs.t/run.t
+++ b/src/programs.t/run.t
@@ -1,5 +1,8 @@
 
   $ hip test_new_entail.ml 2>&1 | grep 'Function\|Entail.*Check' | ./check.py
+  TESTS FAILED
+  ========== Function: test12_false ==========
+  ========== Function: test14_false ==========
 
   $ hip test_new_entail.ml 2>&1 | ./sanitize.sh
   T=>T // norm pre: emp |= emp
@@ -184,6 +187,24 @@
   [Entail  Check] true
   ===========================================
   
+  ex f0 res_1 i_2 f3 i ret. T=>T // pre stage 0: emp |= emp
+  /\ T=>res_1=ret/\0=0 // post stage 0: f0->0 |= i->0
+  /\ T=>i_2=z/\i_2=f3 // norm pre: i->z |= f0->i_2 /\ i_2=f3
+  /\ f3=i_2=>z+1=i_2+1 // norm post: f0->i_2+1 /\ f3=i_2 |= i->z+1
+  /\ res_1=ret // norm res eq: res_1 = ret
+  z3: valid
+  
+  
+  ========== Function: test21_true ==========
+  [Specification] ex i ret; Eff(i->0, [], ret); req i->z; Norm(i->z+1, ret)
+  [Normed   Spec] ex i ret; Eff(i->0, [], ret); req i->z; Norm(i->z+1, ret)
+  
+  [Raw Post Spec] Norm(emp, ()); ex f0; Norm(f0->0, f0); ex res_1; Eff(emp, [], res_1); Norm(emp, res_1); ex i_2; req f0->i_2; Norm(f0->i_2, i_2); Norm(emp, i_2+1); ex f3; req f0->f3; Norm(f0->i_2+1, ()); Norm(emp, res_1)
+  [Normed   Post] ex f0 res_1; Eff(f0->0, [], res_1); ex i_2 f3; req f0->i_2 /\ i_2=f3; Norm(f0->i_2+1 /\ f3=i_2, res_1)
+  
+  [Entail  Check] true
+  ===========================================
+  
   ex f0 res_1 i_2 f3 i. T=>T // pre stage 0: emp |= emp
   /\ T=>res_1=ret/\0=0 // post stage 0: f0->0 |= i->0
   /\ T=>i_2=z/\i_2=f3 // norm pre: i->z |= f0->i_2 /\ i_2=f3
@@ -403,3 +424,112 @@
   [Entail  Check] true
   ===========================================
   
+
+  $ hip test_ho.ml 2>&1 | grep 'Function\|Entail.*Check' | ./check.py
+  ALL OK!
+
+  $ hip test_ho.ml 2>&1 | ./sanitize.sh
+  ex f0 n_6 r. T=>T // pre stage 0: emp |= emp
+  /\ T=>f0=r // post stage 0: emp |= emp
+  /\ T=>T // norm pre: emp |= emp
+  /\ T=>T // norm post: emp |= emp
+  /\ n_6=r // norm res eq: n_6 = r
+  z3: valid
+  
+  
+  ========== Function: test1_true ==========
+  [Specification] ex r; f(emp, [1], r); Norm(emp, r)
+  [Normed   Spec] ex r; f(emp, [1], r); Norm(emp, r)
+  
+  [Raw Post Spec] Norm(emp, ()); ex f0; f(emp, [1], f0)
+  [Normed   Post] ex f0; f(emp, [1], f0); ex n_4; Norm(emp, n_4)
+  
+  [Entail  Check] true
+  ==========================================
+  
+  ex f0 f1 n_10 r s. T=>T // pre stage 0: emp |= emp
+  /\ T=>f0=r // post stage 0: emp |= emp
+  /\ T=>T // pre stage 1: emp |= emp
+  /\ T=>f1=s // post stage 1: emp |= emp
+  /\ T=>T // norm pre: emp |= emp
+  /\ T=>T // norm post: emp |= emp
+  /\ n_10=s // norm res eq: n_10 = s
+  z3: valid
+  
+  
+  ========== Function: test2_true ==========
+  [Specification] ex r; ex s; f(emp, [1], r); g(emp, [2], s); Norm(emp, s)
+  [Normed   Spec] ex r s; f(emp, [1], r); g(emp, [2], s); Norm(emp, s)
+  
+  [Raw Post Spec] Norm(emp, ()); ex f0; f(emp, [1], f0); ex f1; g(emp, [1], f1)
+  [Normed   Post] ex f0; f(emp, [1], f0); ex f1; g(emp, [1], f1); ex n_7; Norm(emp, n_7)
+  
+  [Entail  Check] true
+  ==========================================
+  
+  ex f0 f1 n_10 r s. T=>T // pre stage 0: emp |= emp
+  /\ T=>f0=r // post stage 0: emp |= emp
+  /\ T=>T // pre stage 1: emp |= emp
+  /\ T=>f1=s // post stage 1: emp |= emp
+  /\ T=>T // norm pre: emp |= emp
+  /\ T=>T // norm post: emp |= emp
+  /\ n_10=s // norm res eq: n_10 = s
+  z3: valid
+  
+  
+  ========== Function: test3_true ==========
+  [Specification] ex r; ex s; f(emp, [1], r); g(emp, [r], s); Norm(emp, s)
+  [Normed   Spec] ex r s; f(emp, [1], r); g(emp, [r], s); Norm(emp, s)
+  
+  [Raw Post Spec] Norm(emp, ()); ex f0; f(emp, [1], f0); ex f1; g(emp, [f0], f1)
+  [Normed   Post] ex f0; f(emp, [1], f0); ex f1; g(emp, [f0], f1); ex n_7; Norm(emp, n_7)
+  
+  [Entail  Check] true
+  ==========================================
+  
+  ex r_2 r. T=>T // pre stage 0: emp |= emp
+  /\ T=>r_2=r // post stage 0: emp |= emp
+  /\ T=>T // norm pre: emp |= emp
+  /\ T=>T // norm post: emp |= emp
+  /\ r_2=r // norm res eq: r_2 = r
+  z3: valid
+  
+  
+  ========== Function: test4_true ==========
+  [Specification] ex r; test4_true(emp, [()], r); Norm(emp, r)
+  [Normed   Spec] ex r; test4_true(emp, [()], r); Norm(emp, r)
+  
+  [Raw Post Spec] Norm(emp, ()); ex r_2; test4_true(emp, [()], r_2); Norm(emp, r_2)
+  [Normed   Post] ex r_2; test4_true(emp, [()], r_2); Norm(emp, r_2)
+  
+  [Entail  Check] true
+  ==========================================
+  
+  T=>T // norm pre: emp |= emp
+  /\ b=0=>T // norm post: b=0 |= emp
+  /\ 0=0 // norm res eq: 0 = 0
+  z3: valid
+  
+  T=>T // norm pre: emp |= emp
+  /\ !b=0=>T // norm post: !b=0 |= emp
+  /\ 0=0 // norm res eq: 0 = 0
+  z3: valid
+  
+  ex r_3 r. T=>T // pre stage 0: emp |= emp
+  /\ !b=0=>r_3=r // post stage 0: !b=0 |= emp
+  /\ T=>T // norm pre: emp |= emp
+  /\ T=>T // norm post: emp |= emp
+  /\ r_3=r // norm res eq: r_3 = r
+  z3: valid
+  
+  
+  ========== Function: test5_true ==========
+  [Specification] Norm(emp, 0) \/ ex r; test5_true(emp, [b; n-1], r); Norm(emp, r)
+  [Normed   Spec] Norm(emp, 0) \/ ex r; test5_true(emp, [b; n-1], r); Norm(emp, r)
+  
+  [Raw Post Spec] Norm(emp, ()); Norm(b=0, ()); Norm(emp, 0) \/ Norm(emp, ()); Norm(!b=0, ()); Norm(emp, n-1); Norm(emp, 0) \/ Norm(emp, ()); Norm(!b=0, ()); Norm(emp, n-1); ex r_3; test5_true(emp, [b; n-1-1], r_3); Norm(emp, r_3)
+  [Normed   Post] Norm(b=0, 0) \/ Norm(!b=0, 0) \/ ex r_3; test5_true(!b=0, [b; n-1-1], r_3); Norm(emp, r_3)
+  
+  [Entail  Check] true
+  ==========================================
+  
diff --git a/src/programs.t/test_ho.ml b/src/programs.t/test_ho.ml
new file mode 100644
index 00000000..b1fed382
--- /dev/null
+++ b/src/programs.t/test_ho.ml
@@ -0,0 +1,22 @@
+
+let test1_true f
+  (*@ ex r; f(1, r); Norm(emp, r) @*) =
+  f 1
+
+let test2_true f g
+  (*@ ex r; ex s; f(1, r); g(2, s); Norm(emp, s) @*) =
+  f 1;
+  g 1
+
+let test3_true f g
+  (*@ ex r; ex s; f(1, r); g(r, s); Norm(emp, s) @*) =
+  let x = f 1 in
+  g x
+
+let rec test4_true ()
+  (*@ ex r; test4_true((), r); Norm(emp, r) @*) =
+  test4_true ()
+
+let rec test5_true b n
+  (*@ Norm(emp, 0) \/ ex r; test5_true(b, n-1, r); Norm(emp, r) @*) =
+  if b then 0 else test5_true b (n - 1)
diff --git a/src/programs.t/test_new_entail.ml b/src/programs.t/test_new_entail.ml
index 9a64d69c..b40707c6 100644
--- a/src/programs.t/test_new_entail.ml
+++ b/src/programs.t/test_new_entail.ml
@@ -47,6 +47,18 @@ let test19_true ()  (*@ ex r; Eff(emp, r) @*) =
   let ret = perform Eff in
   1
 
+let test21_true ()  
+(*@ ex i ret;
+   Eff(i->0, ret);
+   req i-> z; 
+   Norm(i->z+1, ret)
+@*)
+= 
+  let i = Sys.opaque_identity (ref 0) in 
+  let ret = perform Eff in 
+  i := !i + 1;
+  ret
+
 let test0_true ()  
 (*@ ex i ;
    Eff(i->0, ret);