val size (e: src_exp) : nat
val size (e: src_exp) : nat
let rec size (e:src_exp)
  : nat
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> 1
    | EIf b e1 e2 -> size b + size e1 + size e2 + 1
    | ELam _ e -> 1 + size e
    | EApp e1 e2 -> 1 + size e1 + size e2
module BoolRefinement
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
#push-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"

let var = nat
let index = nat

let tun = R.pack_ln R.Tv_Unknown

type src_exp =
  | EBVar : index -> src_exp
  | EVar  : var -> src_exp
  | EBool : bool -> src_exp
  | EIf   : src_exp -> src_exp -> src_exp -> src_exp
  | ELam  : src_ty -> src_exp -> src_exp
  | EApp  : src_exp -> src_exp -> src_exp

and src_ty =
  | TBool : src_ty
  | TRefineBool : src_exp -> src_ty
  | TArrow : src_ty -> src_ty -> src_ty
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Tactics.V2.Builtins.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
BoolRefinement.fst
e: BoolRefinement.src_exp -> Prims.nat
BoolRefinement.src_exp Prims.bool BoolRefinement.index BoolRefinement.var Prims.op_Addition BoolRefinement.size BoolRefinement.src_ty Prims.nat
let rec size (e: src_exp) : nat =
  
match e with
| EBool _ | EBVar _ | EVar _ -> 1
| EIf b e1 e2 -> size b + size e1 + size e2 + 1
| ELam _ e -> 1 + size e
| EApp e1 e2 -> 1 + size e1 + size e2