anchor.diff:    (* Zoe: I'm not sure how to use this in our setting since F*'s ast does not
        mark the recursive argument and therefore I'm not sure how to prevent 
        infinite fixpoint unrolling *) 
  +  | FiX of (t -> t) (* Danel: This is a unary rec. def. that will not be unfolded any more *)
   //IN F*: and t : Type0 =
   and t = //JUST FSHARP
     | Lam of (t -> t)
  
positive.code:   | Construct of fv * list<t>
    | Unit
    | Bool of bool
  type head = t
  type annot = option<t> 
  
  (* We are not targeting tagless normalization at this point *)
  let app (f:t) (x:t) =
    match f with
    | Lam f -> f x
    | Accu (a, ts) -> Accu(a, x::ts)
    | Construct(i, ts) -> Construct (i, x::ts)
    | Unit
    | Bool _ -> failwith "Ill-typed application"
  
  let mkConstruct i ts = Construct(i,ts)
  
  
negative.code:     branch :: mkBranches branches' cont
    | _ -> failwith "Unexpected pattern" 
  
  (* We are not targeting tagless normalization at this point *)
  (* Danel: app is now defined simultaneously with translate to accommodate analysing rec. defs. *)
  let rec app (f:t) (x:t) =
    match f with
    | Lam f -> f x
    | Accu (a, ts) -> Accu (a, x::ts)
    | Construct (i, ts) -> Construct (i, x::ts)
    | Rec (y, ts) -> (match x with
                      | Construct (i, ts') -> app (translate (Rec (y, ts)::ts) y) x
                                              (* Danel: if a rec. def. is applied to 
                                                 a constructor, then we unfold it *)
                      | _ -> Accu (FiX (fun (z:t) -> translate (z::ts) y),[x]))
                                                     (* Danel: if a rec. def. is applied 
                                                        to a non-constructor, turn it into 
                                                        an accumulator *)
    | Unit
    | Bool _ -> failwith "Ill-typed application"
  
  and translate (bs:list<t>) (e:term) : t =
      match (SS.compress e).n with
      | Tm_delayed _ -> failwith "Impossible"
  
  