anchor.diff:      | Abs(x,t) -> headonly f t
       | _ -> true in
   
  -  let MAIN_ADMISS_TAC (asl,w as gl) =
  -    let had,args = strip_comb w
  -    if not(is_const had) then failwith "ADMISS_TAC" else
  -    let f,fbod = Choice.get <| dest_abs(last args)
  -    let xtup,bod = Choice.get <| dest_gabs fbod
  -    let hop,args = strip_comb bod
  -    match (name_of had,name_of hop) with
  -      "superadmissible","COND"
  -          -> APPLY_PROFORMA_TAC SUPERADMISSIBLE_COND gl
  -    | "superadmissible","_MATCH" when
  -          name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN"
  -          -> (APPLY_PROFORMA_TAC SUPERADMISSIBLE_MATCH_SEQPATTERN |>THEN<|
  -              CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  -    | "superadmissible","_MATCH" when
  -         is_pattern "_UNGUARDED_PATTERN" 2 (last args)
  -          -> let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
  -             let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN
  -             (APPLY_PROFORMA_TAC th |>THEN<| CONJ_TAC |>THENL<|
  -               [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
  -    | "superadmissible","_MATCH" when
  -         is_pattern "_GUARDED_PATTERN" 3 (last args)
  -          -> let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
  -             let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_GUARDED_PATTERN
  -             (APPLY_PROFORMA_TAC th |>THEN<| CONJ_TAC |>THENL<|
  -               [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
  -    // Choice.get is safe to use after is_*
  -    | "superadmissible",_ when is_comb bod && Choice.get <| rator bod = f -> 
  -             APPLY_PROFORMA_TAC SUPERADMISSIBLE_TAIL gl
  -    | "admissible","sum"
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_SUM gl
  -    | "admissible","nsum"
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_NSUM gl
  -    | "admissible","MAP"
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_MAP gl
  -    | "admissible","_MATCH" when
  -          name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN"
  -          -> (APPLY_PROFORMA_TAC ADMISSIBLE_MATCH_SEQPATTERN |>THEN<|
  -              CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  -    | "admissible","_MATCH"
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_MATCH gl
  -    | "admissible","_UNGUARDED_PATTERN"
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_UNGUARDED_PATTERN gl
  -    | "admissible","_GUARDED_PATTERN"
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_GUARDED_PATTERN gl
  -    | "admissible",_ when is_abs bod
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_LAMBDA gl
  -    // Choice.get is safe to use after is_*
  -    | "admissible",_ when is_comb bod && Choice.get <| rator bod = f -> 
  -            if free_in f (Choice.get <| rand bod) then
  -               APPLY_PROFORMA_TAC ADMISSIBLE_NEST gl
  -             else
  -               APPLY_PROFORMA_TAC ADMISSIBLE_BASE gl
  -    | "admissible",_ when is_comb bod && headonly f bod
  -          -> APPLY_PROFORMA_TAC ADMISSIBLE_COMB gl
  -    | _ -> failwith "MAIN_ADMISS_TAC" in
  -
  -  let ADMISS_TAC =
  -    CONJ_TAC |>ORELSE<|
  -    MATCH_ACCEPT_TAC ADMISSIBLE_CONST |>ORELSE<|
  -    MATCH_ACCEPT_TAC SUPERADMISSIBLE_CONST |>ORELSE<|
  -    MAIN_ADMISS_TAC |>ORELSE<|
  -    MATCH_MP_TAC ADMISSIBLE_IMP_SUPERADMISSIBLE in
  +  let MAIN_ADMISS_TAC(asl, w as gl) = 
  +      let had, args = strip_comb w
  +      if not(is_const had) then failwith "ADMISS_TAC"
  +      else 
  +          let f, fbod = Choice.get <| dest_abs(last args)
  +          let xtup, bod = Choice.get <| dest_gabs fbod
  +          let hop, args = strip_comb bod
  +          match (name_of had, name_of hop) with
  +          | "superadmissible", "COND" -> APPLY_PROFORMA_TAC SUPERADMISSIBLE_COND gl
  +          | "superadmissible", "_MATCH" when name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN" -> 
  +              (APPLY_PROFORMA_TAC SUPERADMISSIBLE_MATCH_SEQPATTERN
  +               |> THEN <| CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  +          | "superadmissible", "_MATCH" when is_pattern "_UNGUARDED_PATTERN" 2 (last args) -> 
  +              let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
  +              let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN
  +              (APPLY_PROFORMA_TAC th
  +               |> THEN <| CONJ_TAC
  +               |> THENL <| [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
  +          | "superadmissible", "_MATCH" when is_pattern "_GUARDED_PATTERN" 3 (last args) -> 
  +              let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
  +              let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_GUARDED_PATTERN
  +              (APPLY_PROFORMA_TAC th
  +               |> THEN <| CONJ_TAC
  +               |> THENL <| [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
  +          // Choice.get is safe to use after is_*
  +          | "superadmissible", _ when is_comb bod && Choice.get <| rator bod = f -> 
  +              APPLY_PROFORMA_TAC SUPERADMISSIBLE_TAIL gl
  +          | "admissible", "sum" -> APPLY_PROFORMA_TAC ADMISSIBLE_SUM gl
  +          | "admissible", "nsum" -> APPLY_PROFORMA_TAC ADMISSIBLE_NSUM gl
  +          | "admissible", "MAP" -> APPLY_PROFORMA_TAC ADMISSIBLE_MAP gl
  +          | "admissible", "_MATCH" when name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN" -> 
  +              (APPLY_PROFORMA_TAC ADMISSIBLE_MATCH_SEQPATTERN
  +               |> THEN <| CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
  +          | "admissible", "_MATCH" -> APPLY_PROFORMA_TAC ADMISSIBLE_MATCH gl
  +          | "admissible", "_UNGUARDED_PATTERN" -> APPLY_PROFORMA_TAC ADMISSIBLE_UNGUARDED_PATTERN gl
  +          | "admissible", "_GUARDED_PATTERN" -> APPLY_PROFORMA_TAC ADMISSIBLE_GUARDED_PATTERN gl
  +          | "admissible", _ when is_abs bod -> APPLY_PROFORMA_TAC ADMISSIBLE_LAMBDA gl
  +          // Choice.get is safe to use after is_*
  +          | "admissible", _ when is_comb bod && Choice.get <| rator bod = f -> 
  +              if free_in f (Choice.get <| rand bod) then APPLY_PROFORMA_TAC ADMISSIBLE_NEST gl
  +              else APPLY_PROFORMA_TAC ADMISSIBLE_BASE gl
  +          | "admissible", _ when is_comb bod && headonly f bod -> APPLY_PROFORMA_TAC ADMISSIBLE_COMB gl
  +          | _ -> failwith "MAIN_ADMISS_TAC"
  +    
  +    in
  +
  +  let ADMISS_TAC = 
  +      CONJ_TAC
  +      |> ORELSE <| MATCH_ACCEPT_TAC ADMISSIBLE_CONST
  +      |> ORELSE <| MATCH_ACCEPT_TAC SUPERADMISSIBLE_CONST
  +      |> ORELSE <| MAIN_ADMISS_TAC
  +      |> ORELSE <| MATCH_MP_TAC ADMISSIBLE_IMP_SUPERADMISSIBLE
  +    
  +    in
   
   (* ------------------------------------------------------------------------- *)
   (* Instantiate the casewise recursion theorem for existential claim.         *)
  
positive.code:          (!f x y. P f x /\ y << G f x ==> y << x) /\
           (!f x. H f x = if P f x then f(G f x) else H' f x)
           ==> ?f. !x. f x = H f x"),
    REPEAT STRIP_TAC |>THEN<| ASM_REWRITE_TAC[] |>THEN<|
    MATCH_MP_TAC WF_REC_TAIL_GENERAL |>THEN<| ASM_MESON_TAC[])
  
  let WF_REC_CASES = 
   prove ((parse_term @"!(<<) clauses.
          WF((<<):A->A->bool) /\
          ALL (\(s,t). ?P G H.
                       (!f a y. P f a /\ y << G f a ==> y << s a) /\
  
negative.code: (* Simplify an existential question about a pattern.                         *)
  (* ------------------------------------------------------------------------- *)
  
    let EXISTS_PAT_CONV = 
        let pth = 
          prove((parse_term @"((?y. _UNGUARDED_PATTERN (GEQ s t) (GEQ z y)) <=> s = t) /\
           ((?y. _GUARDED_PATTERN (GEQ s t) g (GEQ z y)) <=> g /\ s = t)"),
              REWRITE_TAC [_UNGUARDED_PATTERN; _GUARDED_PATTERN; GEQ_DEF]
              |> THEN <| MESON_TAC [])
        let basecnv = GEN_REWRITE_CONV I [pth]
        let pushcnv = GEN_REWRITE_CONV I [SWAP_EXISTS_THM]
        let rec EXISTS_PAT_CONV tm = ((pushcnv
                                       |> THENC <| BINDER_CONV EXISTS_PAT_CONV)
                                       |> ORELSEC <| basecnv) tm
        fun tm -> 
            if is_exists tm then EXISTS_PAT_CONV tm
            else Choice.failwith "EXISTS_PAT_CONV" in
  
  (* ------------------------------------------------------------------------- *)
  (* Hack a proforma to introduce new pairing or pattern variables.            *)
  (* ------------------------------------------------------------------------- *)
  
    let HACK_PROFORMA, EACK_PROFORMA = 
        let elemma0 = 
            prove
                ((parse_term @"((!z. GEQ (f z) (g z)) <=> (!x y. GEQ (f(x,y)) (g(x,y)))) /\ ((\p. P p) = (\(x,y). P(x,y)))"), 
                 REWRITE_TAC [FUN_EQ_THM; FORALL_PAIR_THM])
        let elemma1 = 
            prove((parse_term @"(!P. (!t:A->B->C#D->E. P t) <=> (!t. P (\a b (c,d). t a b d c))) /\
           (!P. (!t:B->C#D->E. P t) <=> (!t. P (\b (c,d). t b d c))) /\
           (!P. (!t:C#D->E. P t) <=> (!t. P (\(c,d). t d c)))"),
                  REPEAT STRIP_TAC
                  |> THEN <| EQ_TAC
                  |> THEN <| REPEAT STRIP_TAC
                  |> THEN <| ASM_REWRITE_TAC []
                  |> THENL <| [FIRST_X_ASSUM(MP_TAC << SPEC(parse_term @"\a b d c. (t:A->B->C#D->E) a b (c,d)"));
                               FIRST_X_ASSUM(MP_TAC << SPEC(parse_term @"\b d c. (t:B->C#D->E) b (c,d)"));
                               FIRST_X_ASSUM(MP_TAC << SPEC(parse_term @"\d c. (t:C#D->E) (c,d)"))]
                  |> THEN <| MATCH_MP_TAC EQ_IMP
                  |> THEN <| AP_TERM_TAC
                  |> THEN <| REWRITE_TAC [FUN_EQ_THM; FORALL_PAIR_THM])
        let HACK_PROFORMA n th = 
            if n <= 1 then th
            else 
                let mkname i = "_P" + string i
                let ty = end_itlist (fun s t -> Choice.get <| mk_type("prod", [s; t])) (map (mk_vartype << mkname) (1 -- n))
                let conv i = 
                    let name = "x" + string i
                    let cnv = ALPHA_CONV(mk_var(name, mk_vartype(mkname i)))
                    fun tm -> 
                    if is_abs tm && name_of(Choice.get <| bndvar tm) <> name then cnv tm
                    else failwith "conv"
                let convs = FIRST_CONV(map conv (1 -- n))
                let th1 = INST_TYPE [ty, (parse_type @"P")] th
                let th2 = REWRITE_RULE [FORALL_PAIR_THM] th1
                let th3 = REWRITE_RULE [elemma0; elemma1] th2
                CONV_RULE (REDEPTH_CONV convs) th3
        let EACK_PROFORMA n th = 
            if n <= 1 then th
            else 
                let mkname i = "_Q" + string i
                let ty = end_itlist (fun s t -> Choice.get <| mk_type("prod", [s; t])) (map (mk_vartype << mkname) (1 -- n))
                let conv i = 
                    let name = "t" + string i
                    let cnv = ALPHA_CONV(mk_var(name, mk_vartype(mkname i)))
                    fun tm -> 
                    if is_abs tm && name_of(Choice.get <| bndvar tm) <> name then cnv tm
                    else failwith "conv"
                let convs = FIRST_CONV(map conv (1 -- n))
                let th1 = INST_TYPE [ty, (parse_type @"Q")] th
                let th2 = REWRITE_RULE [EXISTS_PAIR_THM] th1
                let th3 = REWRITE_RULE [elemma1] th2
                let th4 = REWRITE_RULE [FORALL_PAIR_THM] th3
                CONV_RULE (REDEPTH_CONV convs) th4
        HACK_PROFORMA, EACK_PROFORMA in
  
  (* ------------------------------------------------------------------------- *)
  (* Hack and apply.                                                           *)
  