module Types
  use option.Option
  use int.Int
  use Nat.Nat
  use Functions.Func
  use OptionFuncs.Funcs
  use Sum.Sum
  use Firstorder_symbol_spec.Spec
  use Firstorder_symbol_impl.Types
  use Firstorder_symbol_impl.Logic
  use Firstorder_symbol_impl.Impl
  use Firstorder_term_spec.Spec
  type nl_fo_term_list 'b0 'b3 =
    | NL_FONil
    | NL_FOCons (nl_fo_term 'b0 'b3) (nl_fo_term_list 'b0 'b3)

  with nl_fo_term 'b0 'b3 =
    | NLFVar_fo_term 'b3
    | NLBruijn_fo_term int
    | NL_App (nl_symbol 'b0) (nl_fo_term_list 'b0 'b3)

  type nlimpl_fo_term_list =
    { nlrepr_fo_term_list_field : nl_fo_term_list int int ;
      nlfree_var_symbol_set_abstraction_fo_term_list_field : int ;
      nlfree_var_fo_term_set_abstraction_fo_term_list_field : int ;
      ghost model_fo_term_list_field : fo_term_list int int ;
    }

  type nlimpl_fo_term =
    { nlrepr_fo_term_field : nl_fo_term int int ;
      nlfree_var_symbol_set_abstraction_fo_term_field : int ;
      nlfree_var_fo_term_set_abstraction_fo_term_field : int ;
      ghost model_fo_term_field : fo_term int int ;
    }

  type cons_fo_term_list = | NLC_FONil
    | NLC_FOCons (nlimpl_fo_term) (nlimpl_fo_term_list)

  type cons_fo_term = | NLCVar_fo_term int
    | NLC_App (nlimpl_symbol) (nlimpl_fo_term_list)

end

module Logic
  use option.Option
  use int.Int
  use Nat.Nat
  use Functions.Func
  use OptionFuncs.Funcs
  use Sum.Sum
  use Firstorder_symbol_spec.Spec
  use Firstorder_symbol_impl.Types
  use Firstorder_symbol_impl.Logic
  use Firstorder_symbol_impl.Impl
  use Firstorder_term_spec.Spec
  use Types
  function nat_nlsize_fo_term_list (t:nl_fo_term_list 'b0 'b3) : nat =
    match t with | NL_FONil -> let s = one_nat in s
      | NL_FOCons v0 v1 ->
        let s = one_nat in let s = add_nat (nat_nlsize_fo_term_list v1) s in
          let s = add_nat (nat_nlsize_fo_term v0) s in s
    end

  with nat_nlsize_fo_term (t:nl_fo_term 'b0 'b3) : nat =
    match t with | NLFVar_fo_term v0 -> one_nat
      | NLBruijn_fo_term v0 -> one_nat
      | NL_App v0 v1 ->
        let s = one_nat in let s = add_nat (nat_nlsize_fo_term_list v1) s in
          let s = add_nat (nat_nlsize_symbol v0) s in s
    end

  with nlsize_fo_term_list (t:nl_fo_term_list 'b0 'b3) : int =
    match t with | NL_FONil -> let s = 1 in s
      | NL_FOCons v0 v1 ->
        let s = 1 in let s = nlsize_fo_term_list v1 + s in
          let s = nlsize_fo_term v0 + s in s
    end

  with nlsize_fo_term (t:nl_fo_term 'b0 'b3) : int =
    match t with | NLFVar_fo_term v0 -> 1 | NLBruijn_fo_term v0 -> 1
      | NL_App v0 v1 ->
        let s = 1 in let s = nlsize_fo_term_list v1 + s in
          let s = nlsize_symbol v0 + s in s
    end

  let rec lemma nlsize_positive_lemma_fo_term_list
    (t:nl_fo_term_list 'b0 'b3) : unit ensures { nlsize_fo_term_list t > 0 }
    variant { nat_to_int (nat_nlsize_fo_term_list t) } =
    match t with | NL_FONil -> ()
      | NL_FOCons v0 v1 ->
        nlsize_positive_lemma_fo_term v0 ;
          nlsize_positive_lemma_fo_term_list v1 ; ()
    end

  with lemma nlsize_positive_lemma_fo_term (t:nl_fo_term 'b0 'b3) : unit
    ensures { nlsize_fo_term t > 0 }
    variant { nat_to_int (nat_nlsize_fo_term t) } =
    match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
      | NL_App v0 v1 ->
        nlsize_positive_lemma_symbol v0 ;
          nlsize_positive_lemma_fo_term_list v1 ; ()
    end

  (* Abstraction definition axiom :
      function shiftb_fo_term (bnd: int -> (fo_term 'b0 'b3)) :
         int -> (fo_term 'b0 (option 'b3)) =
        (\ i:int.
           if i = 0 then Var_fo_term None
             else rename_fo_term (bnd (i-1)) identity some)*)
  function shiftb_fo_term (bnd: int -> (fo_term 'b0 'b3)) :
     int -> (fo_term 'b0 (option 'b3))
  axiom shiftb_fo_term_definition :
    forall bnd: int -> (fo_term 'b0 'b3), i:int.
      eval (shiftb_fo_term bnd) i =
        if i = 0 then Var_fo_term None
          else rename_fo_term (bnd (i-1)) identity some

  let lemma shiftb_compose_lemma_fo_term (bnd: int -> (fo_term 'b0 'b3))
    (s0:'b0 -> (symbol 'c0)) (s3:'b3 -> (fo_term 'c0 'c3)) : unit
    ensures {
      subst_compose_fo_term (shiftb_fo_term bnd)
        (rename_subst_symbol s0 identity) (olifts_fo_term s3)
      = shiftb_fo_term (subst_compose_fo_term bnd s0 s3) }
    =
    assert {
      forall i:int. (i = 0 \/ i <> 0) ->
        subst_fo_term (shiftb_fo_term bnd i)
          (rename_subst_symbol s0 identity) (olifts_fo_term s3)
        = eval (shiftb_fo_term (subst_compose_fo_term bnd s0 s3)) i
      } ;
    assert {
      extensionalEqual
        (subst_compose_fo_term (shiftb_fo_term bnd)
           (rename_subst_symbol s0 identity) (olifts_fo_term s3))
        (shiftb_fo_term (subst_compose_fo_term bnd s0 s3))
      }

  function nlmodel_fo_term_list (t:nl_fo_term_list 'b0 'b3)
    (fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0))
    (fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3)) :
    fo_term_list 'c0 'c3 =
    match t with | NL_FONil -> FONil
      | NL_FOCons v0 v1 ->
        FOCons
          (nlmodel_fo_term v0 ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd0 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd3 identity identity)))
          (nlmodel_fo_term_list v1 ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd0 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd3 identity identity)))
    end

  with nlmodel_fo_term (t:nl_fo_term 'b0 'b3) (fr0:'b0 -> (symbol 'c0))
    (bnd0: int -> (symbol 'c0)) (fr3:'b3 -> (fo_term 'c0 'c3))
    (bnd3: int -> (fo_term 'c0 'c3)) : fo_term 'c0 'c3 =
    match t with | NLFVar_fo_term v0 -> fr3 v0
      | NLBruijn_fo_term v0 -> bnd3 v0
      | NL_App v0 v1 ->
        App
          (nlmodel_symbol v0 ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd0 identity)))
          (nlmodel_fo_term_list v1 ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd0 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd3 identity identity)))
    end

  let rec lemma nlmodel_subst_commutation_lemma_fo_term_list
    (t:nl_fo_term_list 'b0 'b3) (fr0:'b0 -> (symbol 'c0))
    (bnd0: int -> (symbol 'c0)) (s0:'c0 -> (symbol 'd0))
    (fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3))
    (s3:'c3 -> (fo_term 'd0 'd3)) : unit
    ensures {
      nlmodel_fo_term_list t (subst_compose_symbol fr0 s0)
        (subst_compose_symbol bnd0 s0) (subst_compose_fo_term fr3 s0 s3)
        (subst_compose_fo_term bnd3 s0 s3)
      = subst_fo_term_list (nlmodel_fo_term_list t fr0 bnd0 fr3 bnd3) s0 s3 }
    variant { nlsize_fo_term_list t } =
    match t with | NL_FONil -> ()
      | NL_FOCons v0 v1 ->
        nlmodel_subst_commutation_lemma_fo_term v0
          ((rename_subst_symbol fr0 identity))
          ((rename_subst_symbol bnd0 identity))
          ((rename_subst_symbol s0 identity))
          ((rename_subst_fo_term fr3 identity identity))
          ((rename_subst_fo_term bnd3 identity identity))
          ((rename_subst_fo_term s3 identity identity)) ;
          assert {
            subst_compose_symbol (rename_subst_symbol fr0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
          assert {
            subst_compose_symbol (rename_subst_symbol bnd0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol bnd0  s0) identity)
            } ;
          assert {
            subst_compose_fo_term
              (rename_subst_fo_term fr3 identity identity)
              ((rename_subst_symbol s0 identity))
              ((rename_subst_fo_term s3 identity identity))
            =
            (rename_subst_fo_term (subst_compose_fo_term fr3 s0 s3) identity
              identity)
            } ;
          assert {
            subst_compose_fo_term
              (rename_subst_fo_term bnd3 identity identity)
              ((rename_subst_symbol s0 identity))
              ((rename_subst_fo_term s3 identity identity))
            =
            (rename_subst_fo_term (subst_compose_fo_term bnd3  s0 s3)
              identity identity)
            } ;
          nlmodel_subst_commutation_lemma_fo_term_list v1
          ((rename_subst_symbol fr0 identity))
          ((rename_subst_symbol bnd0 identity))
          ((rename_subst_symbol s0 identity))
          ((rename_subst_fo_term fr3 identity identity))
          ((rename_subst_fo_term bnd3 identity identity))
          ((rename_subst_fo_term s3 identity identity)) ;
          assert {
            subst_compose_symbol (rename_subst_symbol fr0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
          assert {
            subst_compose_symbol (rename_subst_symbol bnd0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol bnd0  s0) identity)
            } ;
          assert {
            subst_compose_fo_term
              (rename_subst_fo_term fr3 identity identity)
              ((rename_subst_symbol s0 identity))
              ((rename_subst_fo_term s3 identity identity))
            =
            (rename_subst_fo_term (subst_compose_fo_term fr3 s0 s3) identity
              identity)
            } ;
          assert {
            subst_compose_fo_term
              (rename_subst_fo_term bnd3 identity identity)
              ((rename_subst_symbol s0 identity))
              ((rename_subst_fo_term s3 identity identity))
            =
            (rename_subst_fo_term (subst_compose_fo_term bnd3  s0 s3)
              identity identity)
            } ;
          ()
    end

  with lemma nlmodel_subst_commutation_lemma_fo_term (t:nl_fo_term 'b0 'b3)
    (fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0))
    (s0:'c0 -> (symbol 'd0)) (fr3:'b3 -> (fo_term 'c0 'c3))
    (bnd3: int -> (fo_term 'c0 'c3)) (s3:'c3 -> (fo_term 'd0 'd3)) : unit
    ensures {
      nlmodel_fo_term t (subst_compose_symbol fr0 s0)
        (subst_compose_symbol bnd0 s0) (subst_compose_fo_term fr3 s0 s3)
        (subst_compose_fo_term bnd3 s0 s3)
      = subst_fo_term (nlmodel_fo_term t fr0 bnd0 fr3 bnd3) s0 s3 }
    variant { nlsize_fo_term t } =
    match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
      | NL_App v0 v1 ->
        nlmodel_subst_commutation_lemma_symbol v0
          ((rename_subst_symbol fr0 identity))
          ((rename_subst_symbol bnd0 identity))
          ((rename_subst_symbol s0 identity)) ;
          assert {
            subst_compose_symbol (rename_subst_symbol fr0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
          assert {
            subst_compose_symbol (rename_subst_symbol bnd0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol bnd0  s0) identity)
            } ;
          nlmodel_subst_commutation_lemma_fo_term_list v1
          ((rename_subst_symbol fr0 identity))
          ((rename_subst_symbol bnd0 identity))
          ((rename_subst_symbol s0 identity))
          ((rename_subst_fo_term fr3 identity identity))
          ((rename_subst_fo_term bnd3 identity identity))
          ((rename_subst_fo_term s3 identity identity)) ;
          assert {
            subst_compose_symbol (rename_subst_symbol fr0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
          assert {
            subst_compose_symbol (rename_subst_symbol bnd0 identity)
              ((rename_subst_symbol s0 identity))
            = (rename_subst_symbol (subst_compose_symbol bnd0  s0) identity)
            } ;
          assert {
            subst_compose_fo_term
              (rename_subst_fo_term fr3 identity identity)
              ((rename_subst_symbol s0 identity))
              ((rename_subst_fo_term s3 identity identity))
            =
            (rename_subst_fo_term (subst_compose_fo_term fr3 s0 s3) identity
              identity)
            } ;
          assert {
            subst_compose_fo_term
              (rename_subst_fo_term bnd3 identity identity)
              ((rename_subst_symbol s0 identity))
              ((rename_subst_fo_term s3 identity identity))
            =
            (rename_subst_fo_term (subst_compose_fo_term bnd3  s0 s3)
              identity identity)
            } ;
          ()
    end

  let lemma nlmodel_rename_commutation_lemma_fo_term_list
    (t:nl_fo_term_list 'b0 'b3) (fr0:'b0 -> (symbol 'c0))
    (bnd0: int -> (symbol 'c0)) (s0:'c0 -> 'd0)
    (fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3))
    (s3:'c3 -> 'd3) : unit
    ensures {
      nlmodel_fo_term_list t (rename_subst_symbol fr0 s0)
        (rename_subst_symbol bnd0 s0) (rename_subst_fo_term fr3 s0 s3)
        (rename_subst_fo_term bnd3 s0 s3)
      = rename_fo_term_list (nlmodel_fo_term_list t fr0 bnd0 fr3 bnd3) s0 s3
      }
    =
    nlmodel_subst_commutation_lemma_fo_term_list t fr0 bnd0
      (subst_of_rename_symbol s0) fr3 bnd3 (subst_of_rename_fo_term s3)

  let lemma nlmodel_rename_commutation_lemma_fo_term (t:nl_fo_term 'b0 'b3)
    (fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0)) (s0:'c0 -> 'd0)
    (fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3))
    (s3:'c3 -> 'd3) : unit
    ensures {
      nlmodel_fo_term t (rename_subst_symbol fr0 s0)
        (rename_subst_symbol bnd0 s0) (rename_subst_fo_term fr3 s0 s3)
        (rename_subst_fo_term bnd3 s0 s3)
      = rename_fo_term (nlmodel_fo_term t fr0 bnd0 fr3 bnd3) s0 s3 }
    =
    nlmodel_subst_commutation_lemma_fo_term t fr0 bnd0
      (subst_of_rename_symbol s0) fr3 bnd3 (subst_of_rename_fo_term s3)

  predicate correct_indexes_fo_term_list (t:nl_fo_term_list 'b0 'b3) =
    match t with | NL_FONil -> true
      | NL_FOCons v0 v1 ->
        correct_indexes_fo_term v0 /\ correct_indexes_fo_term_list v1
    end

  with correct_indexes_fo_term (t:nl_fo_term 'b0 'b3) =
    match t with | NLFVar_fo_term v0 -> true | NLBruijn_fo_term v0 -> v0 >= 0
      | NL_App v0 v1 ->
        correct_indexes_symbol v0 /\ correct_indexes_fo_term_list v1
    end

  function bound_depth_of_symbol_in_fo_term_list
    (t:nl_fo_term_list 'b0 'b3) : int =
    match t with | NL_FONil -> 0
      | NL_FOCons v0 v1 ->
        let b = bound_depth_of_symbol_in_fo_term v0 in let a = b in
          let b = bound_depth_of_symbol_in_fo_term_list v1 in
          let a = if a > b then a else b in a
    end

  with bound_depth_of_fo_term_in_fo_term_list (t:nl_fo_term_list 'b0 'b3) :
    int =
    match t with | NL_FONil -> 0
      | NL_FOCons v0 v1 ->
        let b = bound_depth_of_fo_term_in_fo_term v0 in let a = b in
          let b = bound_depth_of_fo_term_in_fo_term_list v1 in
          let a = if a > b then a else b in a
    end

  with bound_depth_of_symbol_in_fo_term (t:nl_fo_term 'b0 'b3) : int =
    match t with | NLFVar_fo_term v0 -> 0 | NLBruijn_fo_term v0 -> 0
      | NL_App v0 v1 ->
        let b = bound_depth_of_symbol_in_symbol v0 in let a = b in
          let b = bound_depth_of_symbol_in_fo_term_list v1 in
          let a = if a > b then a else b in a
    end

  with bound_depth_of_fo_term_in_fo_term (t:nl_fo_term 'b0 'b3) : int =
    match t with | NLFVar_fo_term v0 -> 0 | NLBruijn_fo_term v0 -> 1 + v0
      | NL_App v0 v1 ->
        let b = bound_depth_of_fo_term_in_fo_term_list v1 in let a = b in a
    end

  let rec lemma bound_depth_of_symbol_in_fo_term_list_nonnegative
    (t:nl_fo_term_list 'b0 'b3) : unit
    requires { correct_indexes_fo_term_list t }
    ensures { bound_depth_of_symbol_in_fo_term_list t >= 0 }
    variant { nlsize_fo_term_list t } =
    match t with | NL_FONil -> ()
      | NL_FOCons v0 v1 ->
        bound_depth_of_symbol_in_fo_term_nonnegative v0 ;
          bound_depth_of_symbol_in_fo_term_list_nonnegative v1 ; ()
    end

  with lemma bound_depth_of_fo_term_in_fo_term_list_nonnegative
    (t:nl_fo_term_list 'b0 'b3) : unit
    requires { correct_indexes_fo_term_list t }
    ensures { bound_depth_of_fo_term_in_fo_term_list t >= 0 }
    variant { nlsize_fo_term_list t } =
    match t with | NL_FONil -> ()
      | NL_FOCons v0 v1 ->
        bound_depth_of_fo_term_in_fo_term_nonnegative v0 ;
          bound_depth_of_fo_term_in_fo_term_list_nonnegative v1 ; ()
    end

  with lemma bound_depth_of_symbol_in_fo_term_nonnegative
    (t:nl_fo_term 'b0 'b3) : unit requires { correct_indexes_fo_term t }
    ensures { bound_depth_of_symbol_in_fo_term t >= 0 }
    variant { nlsize_fo_term t } =
    match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
      | NL_App v0 v1 ->
        bound_depth_of_symbol_in_symbol_nonnegative v0 ;
          bound_depth_of_symbol_in_fo_term_list_nonnegative v1 ; ()
    end

  with lemma bound_depth_of_fo_term_in_fo_term_nonnegative
    (t:nl_fo_term 'b0 'b3) : unit requires { correct_indexes_fo_term t }
    ensures { bound_depth_of_fo_term_in_fo_term t >= 0 }
    variant { nlsize_fo_term t } =
    match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
      | NL_App v0 v1 ->
        () ; bound_depth_of_fo_term_in_fo_term_list_nonnegative v1 ; ()
    end

  let rec lemma model_equal_fo_term_list (t:nl_fo_term_list 'b0 'b3)
    (fr10: 'b0 -> (symbol 'c0)) (fr20: 'b0 -> (symbol 'c0))
    (bnd10: int -> (symbol 'c0)) (bnd20: int -> (symbol 'c0))
    (fr13: 'b3 -> (fo_term 'c0 'c3)) (fr23: 'b3 -> (fo_term 'c0 'c3))
    (bnd13: int -> (fo_term 'c0 'c3)) (bnd23: int -> (fo_term 'c0 'c3)) :
    unit
    requires {
      forall i:int. 0 <= i < bound_depth_of_symbol_in_fo_term_list t ->
        bnd10 i = bnd20 i
      }
    requires { fr10 = fr20 }
    requires {
      forall i:int. 0 <= i < bound_depth_of_fo_term_in_fo_term_list t ->
        bnd13 i = bnd23 i
      }
    requires { fr13 = fr23 } requires { correct_indexes_fo_term_list t }
    ensures { nlmodel_fo_term_list t fr10 bnd10 fr13 bnd13 =
      nlmodel_fo_term_list t fr20 bnd20 fr23 bnd23 }
    variant { nlsize_fo_term_list t } =
    match t with | NL_FONil -> ()
      | NL_FOCons v0 v1 ->
        model_equal_fo_term v0 ((rename_subst_symbol fr10 identity))
          ((rename_subst_symbol fr20 identity))
          ((rename_subst_symbol bnd10 identity))
          ((rename_subst_symbol bnd20 identity))
          ((rename_subst_fo_term fr13 identity identity))
          ((rename_subst_fo_term fr23 identity identity))
          ((rename_subst_fo_term bnd13 identity identity))
          ((rename_subst_fo_term bnd23 identity identity)) ;
          model_equal_fo_term_list v1 ((rename_subst_symbol fr10 identity))
            ((rename_subst_symbol fr20 identity))
            ((rename_subst_symbol bnd10 identity))
            ((rename_subst_symbol bnd20 identity))
            ((rename_subst_fo_term fr13 identity identity))
            ((rename_subst_fo_term fr23 identity identity))
            ((rename_subst_fo_term bnd13 identity identity))
            ((rename_subst_fo_term bnd23 identity identity)) ;
          ()
    end

  with lemma model_equal_fo_term (t:nl_fo_term 'b0 'b3)
    (fr10: 'b0 -> (symbol 'c0)) (fr20: 'b0 -> (symbol 'c0))
    (bnd10: int -> (symbol 'c0)) (bnd20: int -> (symbol 'c0))
    (fr13: 'b3 -> (fo_term 'c0 'c3)) (fr23: 'b3 -> (fo_term 'c0 'c3))
    (bnd13: int -> (fo_term 'c0 'c3)) (bnd23: int -> (fo_term 'c0 'c3)) :
    unit
    requires {
      forall i:int. 0 <= i < bound_depth_of_symbol_in_fo_term t ->  bnd10 i =
        bnd20 i
      }
    requires { fr10 = fr20 }
    requires {
      forall i:int. 0 <= i < bound_depth_of_fo_term_in_fo_term t ->  bnd13 i
        = bnd23 i
      }
    requires { fr13 = fr23 } requires { correct_indexes_fo_term t }
    ensures { nlmodel_fo_term t fr10 bnd10 fr13 bnd13 =
      nlmodel_fo_term t fr20 bnd20 fr23 bnd23 }
    variant { nlsize_fo_term t } =
    match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
      | NL_App v0 v1 ->
        model_equal_symbol v0 ((rename_subst_symbol fr10 identity))
          ((rename_subst_symbol fr20 identity))
          ((rename_subst_symbol bnd10 identity))
          ((rename_subst_symbol bnd20 identity)) ;
          model_equal_fo_term_list v1 ((rename_subst_symbol fr10 identity))
            ((rename_subst_symbol fr20 identity))
            ((rename_subst_symbol bnd10 identity))
            ((rename_subst_symbol bnd20 identity))
            ((rename_subst_fo_term fr13 identity identity))
            ((rename_subst_fo_term fr23 identity identity))
            ((rename_subst_fo_term bnd13 identity identity))
            ((rename_subst_fo_term bnd23 identity identity)) ;
          ()
    end

  predicate nlimpl_fo_term_list_ok (t:nlimpl_fo_term_list) =
    nlmodel_fo_term_list t.nlrepr_fo_term_list_field subst_id_symbol
      (const (Var_symbol ((-1)))) subst_id_fo_term
      (const (Var_fo_term ((-1)))) = t.model_fo_term_list_field
    /\ correct_indexes_fo_term_list t.nlrepr_fo_term_list_field /\
    bound_depth_of_symbol_in_fo_term_list t.nlrepr_fo_term_list_field = 0 /\
    bound_depth_of_fo_term_in_fo_term_list t.nlrepr_fo_term_list_field = 0 /\
    (forall x:int.
       is_symbol_free_var_in_fo_term_list x t.model_fo_term_list_field -> (x)
       < (t.nlfree_var_symbol_set_abstraction_fo_term_list_field))
    /\
    (forall x:int.
       is_fo_term_free_var_in_fo_term_list x t.model_fo_term_list_field ->
       (x) < (t.nlfree_var_fo_term_set_abstraction_fo_term_list_field))

  predicate nlimpl_fo_term_ok (t:nlimpl_fo_term) =
    nlmodel_fo_term t.nlrepr_fo_term_field subst_id_symbol
      (const (Var_symbol ((-1)))) subst_id_fo_term
      (const (Var_fo_term ((-1)))) = t.model_fo_term_field
    /\ correct_indexes_fo_term t.nlrepr_fo_term_field /\
    bound_depth_of_symbol_in_fo_term t.nlrepr_fo_term_field = 0 /\
    bound_depth_of_fo_term_in_fo_term t.nlrepr_fo_term_field = 0 /\
    (forall x:int. is_symbol_free_var_in_fo_term x t.model_fo_term_field ->
       (x) < (t.nlfree_var_symbol_set_abstraction_fo_term_field))
    /\
    (forall x:int. is_fo_term_free_var_in_fo_term x t.model_fo_term_field ->
       (x) < (t.nlfree_var_fo_term_set_abstraction_fo_term_field))

  predicate cons_ok_fo_term_list (c:cons_fo_term_list) =
    match c with | NLC_FONil -> true
      | NLC_FOCons v0 v1 -> nlimpl_fo_term_ok v0 /\ nlimpl_fo_term_list_ok v1
    end

  predicate cons_ok_fo_term (c:cons_fo_term) =
    match c with | NLCVar_fo_term v0 -> true
      | NLC_App v0 v1 -> nlimpl_symbol_ok v0 /\ nlimpl_fo_term_list_ok v1
    end

  predicate cons_rel_fo_term_list (c:cons_fo_term_list)
    (t:nlimpl_fo_term_list) =
    match c with | NLC_FONil -> t.model_fo_term_list_field = FONil
      | NLC_FOCons v0 v1 -> t.model_fo_term_list_field =
        FOCons (rename_fo_term v0.model_fo_term_field identity identity)
          (rename_fo_term_list v1.model_fo_term_list_field identity identity)
    end

  predicate cons_rel_fo_term (c:cons_fo_term) (t:nlimpl_fo_term) =
    match c with
      | NLCVar_fo_term v0 -> t.model_fo_term_field = Var_fo_term v0
      | NLC_App v0 v1 -> t.model_fo_term_field =
        App (rename_symbol v0.model_symbol_field identity)
          (rename_fo_term_list v1.model_fo_term_list_field identity identity)
    end

  predicate cons_open_rel_fo_term_list (c:cons_fo_term_list)
    (t:nlimpl_fo_term_list) =
    match c with
      | NLC_FONil ->
        match t.model_fo_term_list_field with | FONil -> true
          | FOCons w0 w1 -> false
        end
      | NLC_FOCons v0 v1 ->
        match t.model_fo_term_list_field with | FONil -> false
          | FOCons w0 w1 ->
            v0.model_fo_term_field = (rename_fo_term w0 identity identity) /\
              v1.model_fo_term_list_field =
                (rename_fo_term_list w1 identity identity)
        end
    end

  predicate cons_open_rel_fo_term (c:cons_fo_term) (t:nlimpl_fo_term) =
    match c with
      | NLCVar_fo_term v0 -> t.model_fo_term_field = Var_fo_term v0
      | NLC_App v0 v1 ->
        match t.model_fo_term_field with | Var_fo_term w0 -> false
          | App w0 w1 ->
            v0.model_symbol_field = (rename_symbol w0 identity) /\
              v1.model_fo_term_list_field =
                (rename_fo_term_list w1 identity identity)
        end
    end

end

module Impl
  use option.Option
  use int.Int
  use Nat.Nat
  use Functions.Func
  use OptionFuncs.Funcs
  use Sum.Sum
  use Firstorder_symbol_spec.Spec
  use Firstorder_symbol_impl.Types
  use Firstorder_symbol_impl.Logic
  use Firstorder_symbol_impl.Impl
  use Firstorder_term_spec.Spec
  use Types
  use Logic
  let rec bind_var_symbol_in_fo_term_list (t:nl_fo_term_list int int) (x:int)
    (i:int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd0: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
    requires { correct_indexes_fo_term_list t }
    requires { bound_depth_of_symbol_in_fo_term_list t <= i }
    variant { nlsize_fo_term_list t }
    ensures { bound_depth_of_symbol_in_fo_term_list result <= i + 1 }
    ensures { correct_indexes_fo_term_list result }
    ensures { bound_depth_of_fo_term_in_fo_term_list t =
      bound_depth_of_fo_term_in_fo_term_list result }
    ensures { nlmodel_fo_term_list result fr0 bnd0 fr3 bnd3 =
      nlmodel_fo_term_list t (update fr0 x (bnd0 i)) bnd0 fr3 bnd3 }
    =
    match t with | NL_FONil -> NL_FONil
      | NL_FOCons v0 v1 ->
        assert { (rename_symbol (bnd0 i) identity) =
          (eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
              ((update ((rename_subst_symbol fr0 identity)) x
                  (rename_symbol (bnd0 i) identity)))
            };
          assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
            (update ((rename_subst_symbol fr0 identity)) x
               (eval ((rename_subst_symbol bnd0 identity)) (i+0)))
            };
          assert { (rename_symbol (bnd0 i) identity) =
            (eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
              ((update ((rename_subst_symbol fr0 identity)) x
                  (rename_symbol (bnd0 i) identity)))
            };
          assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
            (update ((rename_subst_symbol fr0 identity)) x
               (eval ((rename_subst_symbol bnd0 identity)) (i+0)))
            };
          NL_FOCons
            (bind_var_symbol_in_fo_term v0 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd3 identity identity)))
            (bind_var_symbol_in_fo_term_list v1 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd3 identity identity)))
    end

  with bind_var_fo_term_in_fo_term_list (t:nl_fo_term_list int int) (x:int)
    (i:int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd0: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
    requires { correct_indexes_fo_term_list t }
    requires { bound_depth_of_fo_term_in_fo_term_list t <= i }
    variant { nlsize_fo_term_list t }
    ensures { bound_depth_of_fo_term_in_fo_term_list result <= i + 1 }
    ensures { correct_indexes_fo_term_list result }
    ensures { bound_depth_of_symbol_in_fo_term_list t =
      bound_depth_of_symbol_in_fo_term_list result }
    ensures { nlmodel_fo_term_list result fr0 bnd0 fr3 bnd3 =
      nlmodel_fo_term_list t fr0 bnd0 (update fr3 x (bnd3 i)) bnd3 }
    =
    match t with | NL_FONil -> NL_FONil
      | NL_FOCons v0 v1 ->
        assert { (rename_fo_term (bnd3 i) identity identity) =
          (eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_fo_term (update fr3 x (bnd3 i)) identity
                 identity))
              ((update ((rename_subst_fo_term fr3 identity identity)) x
                  (rename_fo_term (bnd3 i) identity identity)))
            };
          assert {
            (rename_subst_fo_term (update fr3 x (bnd3 i)) identity identity)
            =
            (update ((rename_subst_fo_term fr3 identity identity)) x
               (eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)))
            };
          assert { (rename_fo_term (bnd3 i) identity identity) =
            (eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_fo_term (update fr3 x (bnd3 i)) identity
                 identity))
              ((update ((rename_subst_fo_term fr3 identity identity)) x
                  (rename_fo_term (bnd3 i) identity identity)))
            };
          assert {
            (rename_subst_fo_term (update fr3 x (bnd3 i)) identity identity)
            =
            (update ((rename_subst_fo_term fr3 identity identity)) x
               (eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)))
            };
          NL_FOCons
            (bind_var_fo_term_in_fo_term v0 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd3 identity identity)))
            (bind_var_fo_term_in_fo_term_list v1 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd3 identity identity)))
    end

  with bind_var_symbol_in_fo_term (t:nl_fo_term int int) (x:int) (i:int)
    (ghost fr0: int -> (symbol 'b0)) (ghost bnd0: int -> (symbol 'b0))
    (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
    requires { correct_indexes_fo_term t }
    requires { bound_depth_of_symbol_in_fo_term t <= i }
    variant { nlsize_fo_term t }
    ensures { bound_depth_of_symbol_in_fo_term result <= i + 1 }
    ensures { correct_indexes_fo_term result }
    ensures { bound_depth_of_fo_term_in_fo_term t =
      bound_depth_of_fo_term_in_fo_term result }
    ensures { nlmodel_fo_term result fr0 bnd0 fr3 bnd3 =
      nlmodel_fo_term t (update fr0 x (bnd0 i)) bnd0 fr3 bnd3 }
    =
    match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
      | NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
      | NL_App v0 v1 ->
        assert { (rename_symbol (bnd0 i) identity) =
          (eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
              ((update ((rename_subst_symbol fr0 identity)) x
                  (rename_symbol (bnd0 i) identity)))
            };
          assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
            (update ((rename_subst_symbol fr0 identity)) x
               (eval ((rename_subst_symbol bnd0 identity)) (i+0)))
            };
          assert { (rename_symbol (bnd0 i) identity) =
            (eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
              ((update ((rename_subst_symbol fr0 identity)) x
                  (rename_symbol (bnd0 i) identity)))
            };
          assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
            (update ((rename_subst_symbol fr0 identity)) x
               (eval ((rename_subst_symbol bnd0 identity)) (i+0)))
            };
          NL_App
            (bind_var_symbol_in_symbol v0 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity)))
            (bind_var_symbol_in_fo_term_list v1 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd3 identity identity)))
    end

  with bind_var_fo_term_in_fo_term (t:nl_fo_term int int) (x:int) (i:int)
    (ghost fr0: int -> (symbol 'b0)) (ghost bnd0: int -> (symbol 'b0))
    (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
    requires { correct_indexes_fo_term t }
    requires { bound_depth_of_fo_term_in_fo_term t <= i }
    variant { nlsize_fo_term t }
    ensures { bound_depth_of_fo_term_in_fo_term result <= i + 1 }
    ensures { correct_indexes_fo_term result }
    ensures { bound_depth_of_symbol_in_fo_term t =
      bound_depth_of_symbol_in_fo_term result }
    ensures { nlmodel_fo_term result fr0 bnd0 fr3 bnd3 =
      nlmodel_fo_term t fr0 bnd0 (update fr3 x (bnd3 i)) bnd3 }
    =
    match t with
      | NLFVar_fo_term v0 ->
        if v0 = x then NLBruijn_fo_term i else NLFVar_fo_term v0
      | NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
      | NL_App v0 v1 ->
        assert { (rename_fo_term (bnd3 i) identity identity) =
          (eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)) };
          assert {
            extensionalEqual
              ((rename_subst_fo_term (update fr3 x (bnd3 i)) identity
                 identity))
              ((update ((rename_subst_fo_term fr3 identity identity)) x
                  (rename_fo_term (bnd3 i) identity identity)))
            };
          assert {
            (rename_subst_fo_term (update fr3 x (bnd3 i)) identity identity)
            =
            (update ((rename_subst_fo_term fr3 identity identity)) x
               (eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)))
            };
          NL_App (v0)
            (bind_var_fo_term_in_fo_term_list v1 x (i+0)
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd0 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd3 identity identity)))
    end

  let rec unbind_var_symbol_in_fo_term_list (t:nl_fo_term_list int int)
    (i:int) (x:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0)) : nl_fo_term_list int int
    requires { i >= 0 } requires { correct_indexes_fo_term_list t }
    requires { bound_depth_of_symbol_in_fo_term_list t <= i + 1 }
    requires { correct_indexes_symbol x }
    requires { bound_depth_of_symbol_in_symbol x = 0 }
    variant { nlsize_fo_term_list t }
    ensures { correct_indexes_fo_term_list result }
    ensures { bound_depth_of_symbol_in_fo_term_list result <= i }
    ensures { bound_depth_of_fo_term_in_fo_term_list result =
      bound_depth_of_fo_term_in_fo_term_list t }
    ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term_list t fr0
        (update bnd10 i (nlmodel_symbol x fr0 bnd20)) fr3 bnd13
      }
    =
    match t with | NL_FONil -> NL_FONil
      | NL_FOCons v0 v1 ->
        assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
          nlmodel_symbol x ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
              (update ((rename_subst_symbol bnd10 identity)) (i+0)
                 (rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol
              (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
            =
            update ((rename_subst_symbol bnd10 identity)) (i+0)
              (nlmodel_symbol x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
            nlmodel_symbol x ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
              (update ((rename_subst_symbol bnd10 identity)) (i+0)
                 (rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol
              (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
            =
            update ((rename_subst_symbol bnd10 identity)) (i+0)
              (nlmodel_symbol x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          NL_FOCons
            (unbind_var_symbol_in_fo_term v0 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity)))
            (unbind_var_symbol_in_fo_term_list v1 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity)))
    end

  with unbind_var_fo_term_in_fo_term_list (t:nl_fo_term_list int int) (i:int)
    (x:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0))
    (ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
    requires { i >= 0 } requires { correct_indexes_fo_term_list t }
    requires { bound_depth_of_fo_term_in_fo_term_list t <= i + 1 }
    requires { correct_indexes_fo_term x }
    requires { bound_depth_of_symbol_in_fo_term x = 0 }
    requires { bound_depth_of_fo_term_in_fo_term x = 0 }
    variant { nlsize_fo_term_list t }
    ensures { correct_indexes_fo_term_list result }
    ensures { bound_depth_of_fo_term_in_fo_term_list result <= i }
    ensures { bound_depth_of_symbol_in_fo_term_list result =
      bound_depth_of_symbol_in_fo_term_list t }
    ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term_list t fr0 bnd10 fr3
        (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
      }
    =
    match t with | NL_FONil -> NL_FONil
      | NL_FOCons v0 v1 ->
        assert {
          rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
            identity
          =
          nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd23 identity identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
                 (rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
              identity identity)
            =
            update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
              (nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          assert {
            rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
              identity
            =
            nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
              ((rename_subst_fo_term fr3 identity identity))
              ((rename_subst_fo_term bnd23 identity identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
                 (rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
              identity identity)
            =
            update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
              (nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          NL_FOCons
            (unbind_var_fo_term_in_fo_term v0 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity))
               ((rename_subst_fo_term bnd23 identity identity)))
            (unbind_var_fo_term_in_fo_term_list v1 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity))
               ((rename_subst_fo_term bnd23 identity identity)))
    end

  with unbind_var_symbol_in_fo_term (t:nl_fo_term int int) (i:int)
    (x:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0)) : nl_fo_term int int
    requires { i >= 0 } requires { correct_indexes_fo_term t }
    requires { bound_depth_of_symbol_in_fo_term t <= i + 1 }
    requires { correct_indexes_symbol x }
    requires { bound_depth_of_symbol_in_symbol x = 0 }
    variant { nlsize_fo_term t }
    ensures { correct_indexes_fo_term result }
    ensures { bound_depth_of_symbol_in_fo_term result <= i }
    ensures { bound_depth_of_fo_term_in_fo_term result =
      bound_depth_of_fo_term_in_fo_term t }
    ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term t fr0 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) fr3
        bnd13
      }
    =
    match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
      | NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
      | NL_App v0 v1 ->
        assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
          nlmodel_symbol x ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
              (update ((rename_subst_symbol bnd10 identity)) (i+0)
                 (rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol
              (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
            =
            update ((rename_subst_symbol bnd10 identity)) (i+0)
              (nlmodel_symbol x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
            nlmodel_symbol x ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
              (update ((rename_subst_symbol bnd10 identity)) (i+0)
                 (rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol
              (update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
            =
            update ((rename_subst_symbol bnd10 identity)) (i+0)
              (nlmodel_symbol x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          NL_App
            (unbind_var_symbol_in_symbol v0 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_symbol bnd20 identity)))
            (unbind_var_symbol_in_fo_term_list v1 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity)))
    end

  with unbind_var_fo_term_in_fo_term (t:nl_fo_term int int) (i:int)
    (x:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0))
    (ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
    requires { i >= 0 } requires { correct_indexes_fo_term t }
    requires { bound_depth_of_fo_term_in_fo_term t <= i + 1 }
    requires { correct_indexes_fo_term x }
    requires { bound_depth_of_symbol_in_fo_term x = 0 }
    requires { bound_depth_of_fo_term_in_fo_term x = 0 }
    variant { nlsize_fo_term t }
    ensures { correct_indexes_fo_term result }
    ensures { bound_depth_of_fo_term_in_fo_term result <= i }
    ensures { bound_depth_of_symbol_in_fo_term result =
      bound_depth_of_symbol_in_fo_term t }
    ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term t fr0 bnd10 fr3
        (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
      }
    =
    match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
      | NLBruijn_fo_term v0 ->
        if v0 = i
          then (model_equal_fo_term x fr0 fr0 bnd10 bnd20 fr3 fr3 bnd13 bnd23 ;
            x)
          else NLBruijn_fo_term v0
      | NL_App v0 v1 ->
        assert {
          rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
            identity
          =
          nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd23 identity identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
                 (rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
              identity identity)
            =
            update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
              (nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          assert {
            rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
              identity
            =
            nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
              ((rename_subst_fo_term fr3 identity identity))
              ((rename_subst_fo_term bnd23 identity identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
                 (rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
              identity identity)
            =
            update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
              (nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          NL_App (v0)
            (unbind_var_fo_term_in_fo_term_list v1 (i+0) x
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity))
               ((rename_subst_fo_term bnd23 identity identity)))
    end

  let rec subst_base_symbol_in_fo_term_list (t:nl_fo_term_list int int)
    (x:int) (u:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0)) : nl_fo_term_list int int
    requires { correct_indexes_fo_term_list t }
    requires { correct_indexes_symbol u }
    requires { bound_depth_of_symbol_in_symbol u = 0 }
    variant { nlsize_fo_term_list t }
    ensures { correct_indexes_fo_term_list result }
     ensures { bound_depth_of_symbol_in_fo_term_list result =
       bound_depth_of_symbol_in_fo_term_list t }
    ensures { bound_depth_of_fo_term_in_fo_term_list result =
      bound_depth_of_fo_term_in_fo_term_list t }
    ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term_list t (update fr0 x (nlmodel_symbol u fr0 bnd20))
        bnd10 fr3 bnd13
      }
    =
    match t with | NL_FONil -> NL_FONil
      | NL_FOCons v0 v1 ->
        assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
          nlmodel_symbol u ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
              (update ((rename_subst_symbol fr0 identity)) x
                 (rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
              identity)
            =
            update ((rename_subst_symbol fr0 identity)) x
              (nlmodel_symbol u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
            nlmodel_symbol u ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
              (update ((rename_subst_symbol fr0 identity)) x
                 (rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
              identity)
            =
            update ((rename_subst_symbol fr0 identity)) x
              (nlmodel_symbol u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          NL_FOCons
            (subst_base_symbol_in_fo_term v0 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity)))
            (subst_base_symbol_in_fo_term_list v1 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity)))
    end

  with subst_base_fo_term_in_fo_term_list (t:nl_fo_term_list int int) (x:int)
    (u:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0))
    (ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
    requires { correct_indexes_fo_term_list t }
    requires { correct_indexes_fo_term u }
    requires { bound_depth_of_symbol_in_fo_term u = 0 }
    requires { bound_depth_of_fo_term_in_fo_term u = 0 }
    variant { nlsize_fo_term_list t }
    ensures { correct_indexes_fo_term_list result }
     ensures { bound_depth_of_symbol_in_fo_term_list result =
       bound_depth_of_symbol_in_fo_term_list t }
    ensures { bound_depth_of_fo_term_in_fo_term_list result =
      bound_depth_of_fo_term_in_fo_term_list t }
    ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term_list t fr0 bnd10
        (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) bnd13
      }
    =
    match t with | NL_FONil -> NL_FONil
      | NL_FOCons v0 v1 ->
        assert {
          rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
            identity
          =
          nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd23 identity identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term fr3 identity identity)) x
                 (rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
              identity)
            =
            update ((rename_subst_fo_term fr3 identity identity)) x
              (nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          assert {
            rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
              identity
            =
            nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
              ((rename_subst_fo_term fr3 identity identity))
              ((rename_subst_fo_term bnd23 identity identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term fr3 identity identity)) x
                 (rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
              identity)
            =
            update ((rename_subst_fo_term fr3 identity identity)) x
              (nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          NL_FOCons
            (subst_base_fo_term_in_fo_term v0 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity))
               ((rename_subst_fo_term bnd23 identity identity)))
            (subst_base_fo_term_in_fo_term_list v1 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity))
               ((rename_subst_fo_term bnd23 identity identity)))
    end

  with subst_base_symbol_in_fo_term (t:nl_fo_term int int) (x:int)
    (u:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0)) : nl_fo_term int int
    requires { correct_indexes_fo_term t }
    requires { correct_indexes_symbol u }
    requires { bound_depth_of_symbol_in_symbol u = 0 }
    variant { nlsize_fo_term t }
    ensures { correct_indexes_fo_term result }
     ensures { bound_depth_of_symbol_in_fo_term result =
       bound_depth_of_symbol_in_fo_term t }
    ensures { bound_depth_of_fo_term_in_fo_term result =
      bound_depth_of_fo_term_in_fo_term t }
    ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term t (update fr0 x (nlmodel_symbol u fr0 bnd20)) bnd10 fr3
        bnd13
      }
    =
    match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
      | NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
      | NL_App v0 v1 ->
        assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
          nlmodel_symbol u ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
              (update ((rename_subst_symbol fr0 identity)) x
                 (rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
              identity)
            =
            update ((rename_subst_symbol fr0 identity)) x
              (nlmodel_symbol u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
            nlmodel_symbol u ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_symbol
                 (update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
              (update ((rename_subst_symbol fr0 identity)) x
                 (rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
            } ;
          assert {
            (rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
              identity)
            =
            update ((rename_subst_symbol fr0 identity)) x
              (nlmodel_symbol u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity)))
            } ;
          NL_App
            (subst_base_symbol_in_symbol v0 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_symbol bnd20 identity)))
            (subst_base_symbol_in_fo_term_list v1 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity)))
    end

  with subst_base_fo_term_in_fo_term (t:nl_fo_term int int) (x:int)
    (u:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
    (ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
    (ghost bnd13: int -> (fo_term 'b0 'b3))
    (ghost bnd20: int -> (symbol 'b0))
    (ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
    requires { correct_indexes_fo_term t }
    requires { correct_indexes_fo_term u }
    requires { bound_depth_of_symbol_in_fo_term u = 0 }
    requires { bound_depth_of_fo_term_in_fo_term u = 0 }
    variant { nlsize_fo_term t }
    ensures { correct_indexes_fo_term result }
     ensures { bound_depth_of_symbol_in_fo_term result =
       bound_depth_of_symbol_in_fo_term t }
    ensures { bound_depth_of_fo_term_in_fo_term result =
      bound_depth_of_fo_term_in_fo_term t }
    ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
      nlmodel_fo_term t fr0 bnd10
        (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) bnd13
      }
    =
    match t with
      | NLFVar_fo_term v0 ->
        if v0 = x
          then (model_equal_fo_term u fr0 fr0 bnd10 bnd20 fr3 fr3 bnd13 bnd23 ;
            u)
          else NLFVar_fo_term v0
      | NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
      | NL_App v0 v1 ->
        assert {
          rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
            identity
          =
          nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
            ((rename_subst_symbol bnd20 identity))
            ((rename_subst_fo_term fr3 identity identity))
            ((rename_subst_fo_term bnd23 identity identity))
          } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term fr3 identity identity)) x
                 (rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
              identity)
            =
            update ((rename_subst_fo_term fr3 identity identity)) x
              (nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          assert {
            rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
              identity
            =
            nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
              ((rename_subst_symbol bnd20 identity))
              ((rename_subst_fo_term fr3 identity identity))
              ((rename_subst_fo_term bnd23 identity identity))
            } ;
          assert {
            extensionalEqual
              ((rename_subst_fo_term
                 (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
                 identity identity))
              (update ((rename_subst_fo_term fr3 identity identity)) x
                 (rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
                    identity identity))
            } ;
          assert {
            (rename_subst_fo_term
              (update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
              identity)
            =
            update ((rename_subst_fo_term fr3 identity identity)) x
              (nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
                 ((rename_subst_symbol bnd20 identity))
                 ((rename_subst_fo_term fr3 identity identity))
                 ((rename_subst_fo_term bnd23 identity identity)))
            } ;
          NL_App (v0)
            (subst_base_fo_term_in_fo_term_list v1 x u
               ((rename_subst_symbol fr0 identity))
               ((rename_subst_symbol bnd10 identity))
               ((rename_subst_fo_term fr3 identity identity))
               ((rename_subst_fo_term bnd13 identity identity))
               ((rename_subst_symbol bnd20 identity))
               ((rename_subst_fo_term bnd23 identity identity)))
    end

  let construct_fo_term_list (c:cons_fo_term_list) : nlimpl_fo_term_list
    requires { cons_ok_fo_term_list c }
    ensures { nlimpl_fo_term_list_ok result }
    ensures { cons_rel_fo_term_list c result }
    (*ensures { cons_open_rel_fo_term_list c result }*) =
    match c with
      | NLC_FONil ->
        let res =
          { nlrepr_fo_term_list_field = (NL_FONil) ;
            nlfree_var_symbol_set_abstraction_fo_term_list_field = 0 ;
            nlfree_var_fo_term_set_abstraction_fo_term_list_field = 0 ;
            model_fo_term_list_field = ghost (FONil) ;
          }
        in
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_term_list x res.model_fo_term_list_field
            -> (false) && (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_term_list x
              res.model_fo_term_list_field
            -> (false) && (x) <
            (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
          } ;
        res
      | NLC_FOCons v0 v1 -> assert { nlimpl_fo_term_ok v0 } ;
        assert { nlimpl_fo_term_list_ok v1 } ;
        let res =
          {
            nlrepr_fo_term_list_field =
              (NL_FOCons (let v0 = v0.nlrepr_fo_term_field in v0)
                 (let v1 = v1.nlrepr_fo_term_list_field in v1)) ;
            nlfree_var_symbol_set_abstraction_fo_term_list_field =
              (let aux (a:int) (b:int) : int
                 ensures { result >= a /\ result >= b } =
                 if a < b then b else a in
                 aux (v0.nlfree_var_symbol_set_abstraction_fo_term_field)
                   (v1.nlfree_var_symbol_set_abstraction_fo_term_list_field)) ;
            nlfree_var_fo_term_set_abstraction_fo_term_list_field =
              (let aux (a:int) (b:int) : int
                 ensures { result >= a /\ result >= b } =
                 if a < b then b else a in
                 aux (v0.nlfree_var_fo_term_set_abstraction_fo_term_field)
                   (v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field)) ;
            model_fo_term_list_field = ghost
              (FOCons
                 (rename_fo_term v0.model_fo_term_field identity identity)
                 (rename_fo_term_list v1.model_fo_term_list_field identity
                    identity)) ;
          }
        in
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_term x
              (rename_fo_term v0.model_fo_term_field identity identity)
            ->
            (forall y:int.
               (is_symbol_free_var_in_fo_term y v0.model_fo_term_field /\
               eval (identity) y = x) -> x = eval (identity) y && x = y &&
               is_symbol_free_var_in_fo_term x v0.model_fo_term_field)
            && is_symbol_free_var_in_fo_term x v0.model_fo_term_field && (x)
            < (v0.nlfree_var_symbol_set_abstraction_fo_term_field) && (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_term x
              (rename_fo_term v0.model_fo_term_field identity identity)
            ->
            (forall y:int.
               (is_fo_term_free_var_in_fo_term y v0.model_fo_term_field /\
               eval (identity) y = x) -> x = eval (identity) y && x = y &&
               is_fo_term_free_var_in_fo_term x v0.model_fo_term_field)
            && is_fo_term_free_var_in_fo_term x v0.model_fo_term_field && (x)
            < (v0.nlfree_var_fo_term_set_abstraction_fo_term_field) && (x) <
            (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
          } ;
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_term_list x
              (rename_fo_term_list v1.model_fo_term_list_field identity
                 identity)
            ->
            (forall y:int.
               (is_symbol_free_var_in_fo_term_list y
                  v1.model_fo_term_list_field
               /\ eval (identity) y = x) -> x = eval (identity) y &&
               x = y &&
               is_symbol_free_var_in_fo_term_list x
                 v1.model_fo_term_list_field)
            &&
            is_symbol_free_var_in_fo_term_list x v1.model_fo_term_list_field
            && (x) <
            (v1.nlfree_var_symbol_set_abstraction_fo_term_list_field) && (x)
            < (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_term_list x
              (rename_fo_term_list v1.model_fo_term_list_field identity
                 identity)
            ->
            (forall y:int.
               (is_fo_term_free_var_in_fo_term_list y
                  v1.model_fo_term_list_field
               /\ eval (identity) y = x) -> x = eval (identity) y &&
               x = y &&
               is_fo_term_free_var_in_fo_term_list x
                 v1.model_fo_term_list_field)
            &&
            is_fo_term_free_var_in_fo_term_list x v1.model_fo_term_list_field
            && (x) <
            (v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field) && (x)
            < (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
          } ;
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_term_list x res.model_fo_term_list_field
            ->
            (is_symbol_free_var_in_fo_term x
               (rename_fo_term v0.model_fo_term_field identity identity) \/
               is_symbol_free_var_in_fo_term_list x
                 (rename_fo_term_list v1.model_fo_term_list_field identity
                    identity))
            && (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_term_list x
              res.model_fo_term_list_field
            ->
            (is_fo_term_free_var_in_fo_term x
               (rename_fo_term v0.model_fo_term_field identity identity) \/
               is_fo_term_free_var_in_fo_term_list x
                 (rename_fo_term_list v1.model_fo_term_list_field identity
                    identity))
            && (x) <
            (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
          } ;
        assert {
          extensionalEqual (rename_subst_symbol subst_id_symbol identity)
            ((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
                identity))
          } ;
        assert { rename_subst_symbol subst_id_symbol identity =
          (rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
             identity)
          } ;
        assert {
          extensionalEqual
            (rename_subst_fo_term subst_id_fo_term identity identity)
            ((rename_subst_fo_term
                (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
                identity))
          } ;
        assert { rename_subst_fo_term subst_id_fo_term identity identity =
          (rename_subst_fo_term
             (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
             identity)
          } ;
        model_equal_fo_term v0.nlrepr_fo_term_field
          (rename_subst_symbol subst_id_symbol identity)
          (rename_subst_symbol subst_id_symbol identity)
          ((rename_subst_symbol (const (Var_symbol (-1))) identity))
          (rename_subst_symbol (const (Var_symbol (-1))) identity)
          (rename_subst_fo_term subst_id_fo_term identity identity)
          (rename_subst_fo_term subst_id_fo_term identity identity)
          ((rename_subst_fo_term (const (Var_fo_term (-1))) identity
             identity))
          (rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        assert {
          extensionalEqual (rename_subst_symbol subst_id_symbol identity)
            ((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
                identity))
          } ;
        assert { rename_subst_symbol subst_id_symbol identity =
          (rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
             identity)
          } ;
        assert {
          extensionalEqual
            (rename_subst_fo_term subst_id_fo_term identity identity)
            ((rename_subst_fo_term
                (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
                identity))
          } ;
        assert { rename_subst_fo_term subst_id_fo_term identity identity =
          (rename_subst_fo_term
             (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
             identity)
          } ;
        model_equal_fo_term_list v1.nlrepr_fo_term_list_field
          (rename_subst_symbol subst_id_symbol identity)
          (rename_subst_symbol subst_id_symbol identity)
          ((rename_subst_symbol (const (Var_symbol (-1))) identity))
          (rename_subst_symbol (const (Var_symbol (-1))) identity)
          (rename_subst_fo_term subst_id_fo_term identity identity)
          (rename_subst_fo_term subst_id_fo_term identity identity)
          ((rename_subst_fo_term (const (Var_fo_term (-1))) identity
             identity))
          (rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        res
    end

  let construct_fo_term (c:cons_fo_term) : nlimpl_fo_term
    requires { cons_ok_fo_term c } ensures { nlimpl_fo_term_ok result }
    ensures { cons_rel_fo_term c result }
    (*ensures { cons_open_rel_fo_term c result }*) =
    match c with
      | NLCVar_fo_term v0 ->
        { nlrepr_fo_term_field = NLFVar_fo_term v0 ;
          nlfree_var_symbol_set_abstraction_fo_term_field = 0 ;
          nlfree_var_fo_term_set_abstraction_fo_term_field = (1 + (v0)) ;
          model_fo_term_field = ghost (Var_fo_term v0) ;
        }
      | NLC_App v0 v1 -> assert { nlimpl_symbol_ok v0 } ;
        assert { nlimpl_fo_term_list_ok v1 } ;
        let res =
          {
            nlrepr_fo_term_field =
              (NL_App (let v0 = v0.nlrepr_symbol_field in v0)
                 (let v1 = v1.nlrepr_fo_term_list_field in v1)) ;
            nlfree_var_symbol_set_abstraction_fo_term_field =
              (let aux (a:int) (b:int) : int
                 ensures { result >= a /\ result >= b } =
                 if a < b then b else a in
                 aux (v0.nlfree_var_symbol_set_abstraction_symbol_field)
                   (v1.nlfree_var_symbol_set_abstraction_fo_term_list_field)) ;
            nlfree_var_fo_term_set_abstraction_fo_term_field =
              v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field ;
            model_fo_term_field = ghost
              (App (rename_symbol v0.model_symbol_field identity)
                 (rename_fo_term_list v1.model_fo_term_list_field identity
                    identity)) ;
          }
        in
        assert {
          forall x:int.
            is_symbol_free_var_in_symbol x
              (rename_symbol v0.model_symbol_field identity)
            ->
            (forall y:int.
               (is_symbol_free_var_in_symbol y v0.model_symbol_field /\
               eval (identity) y = x) -> x = eval (identity) y && x = y &&
               is_symbol_free_var_in_symbol x v0.model_symbol_field)
            && is_symbol_free_var_in_symbol x v0.model_symbol_field && (x) <
            (v0.nlfree_var_symbol_set_abstraction_symbol_field) && (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_term_field)
          } ;
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_term_list x
              (rename_fo_term_list v1.model_fo_term_list_field identity
                 identity)
            ->
            (forall y:int.
               (is_symbol_free_var_in_fo_term_list y
                  v1.model_fo_term_list_field
               /\ eval (identity) y = x) -> x = eval (identity) y &&
               x = y &&
               is_symbol_free_var_in_fo_term_list x
                 v1.model_fo_term_list_field)
            &&
            is_symbol_free_var_in_fo_term_list x v1.model_fo_term_list_field
            && (x) <
            (v1.nlfree_var_symbol_set_abstraction_fo_term_list_field) && (x)
            < (res.nlfree_var_symbol_set_abstraction_fo_term_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_term_list x
              (rename_fo_term_list v1.model_fo_term_list_field identity
                 identity)
            ->
            (forall y:int.
               (is_fo_term_free_var_in_fo_term_list y
                  v1.model_fo_term_list_field
               /\ eval (identity) y = x) -> x = eval (identity) y &&
               x = y &&
               is_fo_term_free_var_in_fo_term_list x
                 v1.model_fo_term_list_field)
            &&
            is_fo_term_free_var_in_fo_term_list x v1.model_fo_term_list_field
            && (x) <
            (v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field) && (x)
            < (res.nlfree_var_fo_term_set_abstraction_fo_term_field)
          } ;
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_term x res.model_fo_term_field ->
            (is_symbol_free_var_in_symbol x
               (rename_symbol v0.model_symbol_field identity) \/
               is_symbol_free_var_in_fo_term_list x
                 (rename_fo_term_list v1.model_fo_term_list_field identity
                    identity))
            && (x) < (res.nlfree_var_symbol_set_abstraction_fo_term_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_term x res.model_fo_term_field ->
            (is_fo_term_free_var_in_fo_term_list x
               (rename_fo_term_list v1.model_fo_term_list_field identity
                  identity))
            && (x) < (res.nlfree_var_fo_term_set_abstraction_fo_term_field)
          } ;
        assert {
          extensionalEqual (rename_subst_symbol subst_id_symbol identity)
            ((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
                identity))
          } ;
        assert { rename_subst_symbol subst_id_symbol identity =
          (rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
             identity)
          } ;
        model_equal_symbol v0.nlrepr_symbol_field
          (rename_subst_symbol subst_id_symbol identity)
          (rename_subst_symbol subst_id_symbol identity)
          ((rename_subst_symbol (const (Var_symbol (-1))) identity))
          (rename_subst_symbol (const (Var_symbol (-1))) identity) ;
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        assert {
          extensionalEqual (rename_subst_symbol subst_id_symbol identity)
            ((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
                identity))
          } ;
        assert { rename_subst_symbol subst_id_symbol identity =
          (rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
             identity)
          } ;
        assert {
          extensionalEqual
            (rename_subst_fo_term subst_id_fo_term identity identity)
            ((rename_subst_fo_term
                (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
                identity))
          } ;
        assert { rename_subst_fo_term subst_id_fo_term identity identity =
          (rename_subst_fo_term
             (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
             identity)
          } ;
        model_equal_fo_term_list v1.nlrepr_fo_term_list_field
          (rename_subst_symbol subst_id_symbol identity)
          (rename_subst_symbol subst_id_symbol identity)
          ((rename_subst_symbol (const (Var_symbol (-1))) identity))
          (rename_subst_symbol (const (Var_symbol (-1))) identity)
          (rename_subst_fo_term subst_id_fo_term identity identity)
          (rename_subst_fo_term subst_id_fo_term identity identity)
          ((rename_subst_fo_term (const (Var_fo_term (-1))) identity
             identity))
          (rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        (*assert {
            extensionalEqual (rcompose (identity) (identity))
              ((identity : (int) -> (int)))
            } ;
        assert { rcompose (identity) (identity) = (identity : (int) -> (int))
          } ;*)
        res
    end

  let destruct_fo_term_list (t:nlimpl_fo_term_list) : cons_fo_term_list
    requires { nlimpl_fo_term_list_ok t }
    ensures { cons_ok_fo_term_list result }
    ensures { cons_rel_fo_term_list result t }
    ensures { cons_open_rel_fo_term_list result t } =
    let fv0 = t.nlfree_var_symbol_set_abstraction_fo_term_list_field in
    let fv3 = t.nlfree_var_fo_term_set_abstraction_fo_term_list_field in
    match t.nlrepr_fo_term_list_field with
      | NL_FONil ->
        assert { t.model_fo_term_list_field = FONil } ;
          let () =
            match t.model_fo_term_list_field with | FONil -> ()
              | FOCons x0 x1 -> absurd
            end
          in let res = NLC_FONil in res
      | NL_FOCons v0 v1 ->
        assert { t.model_fo_term_list_field =
          FOCons
            (nlmodel_fo_term v0
               (rename_subst_symbol subst_id_symbol identity)
               (rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity)
               (rename_subst_fo_term subst_id_fo_term identity identity)
               (rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
            (nlmodel_fo_term_list v1
               (rename_subst_symbol subst_id_symbol identity)
               (rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity)
               (rename_subst_fo_term subst_id_fo_term identity identity)
               (rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
          } ;
          let (mv0 , mv1) =
            match t.model_fo_term_list_field with | FONil -> absurd
              | FOCons x0 x1 -> (x0 , x1)
            end
          in
          assert { mv0 =
            nlmodel_fo_term v0
              ((rename_subst_symbol subst_id_symbol identity))
              ((rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity))
              ((rename_subst_fo_term subst_id_fo_term identity identity))
              ((rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
            } ;
          assert { mv1 =
            nlmodel_fo_term_list v1
              ((rename_subst_symbol subst_id_symbol identity))
              ((rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity))
              ((rename_subst_fo_term subst_id_fo_term identity identity))
              ((rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
            } ;
          assert { bound_depth_of_symbol_in_fo_term v0 <= 0 } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_term x mv0 ->
              is_symbol_free_var_in_fo_term_list x t.model_fo_term_list_field
              && (x) <
              (t.nlfree_var_symbol_set_abstraction_fo_term_list_field)
            } ;
          assert { bound_depth_of_fo_term_in_fo_term v0 <= 0 } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_term x mv0 ->
              is_fo_term_free_var_in_fo_term_list x
                t.model_fo_term_list_field
              && (x) <
              (t.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
            } ;
          assert { bound_depth_of_symbol_in_fo_term_list v1 <= 0 } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_term_list x mv1 ->
              is_symbol_free_var_in_fo_term_list x t.model_fo_term_list_field
              && (x) <
              (t.nlfree_var_symbol_set_abstraction_fo_term_list_field)
            } ;
          assert { bound_depth_of_fo_term_in_fo_term_list v1 <= 0 } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_term_list x mv1 ->
              is_fo_term_free_var_in_fo_term_list x
                t.model_fo_term_list_field
              && (x) <
              (t.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
            } ;
          model_equal_fo_term v0 subst_id_symbol
            (rename_subst_symbol
               ((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
            const (Var_symbol (-1)) : int -> (symbol int)))
            (rename_subst_symbol
               ((rename_subst_symbol
                  (const (Var_symbol (-1)) : int -> (symbol int)) identity))
               (identity))
            subst_id_fo_term
            (rename_subst_fo_term
               ((rename_subst_fo_term subst_id_fo_term identity identity))
               (identity) (identity)) ((const (Var_fo_term (-1)) :
                                          int -> (fo_term int int)))
            (rename_subst_fo_term
               ((rename_subst_fo_term
                  (const (Var_fo_term (-1)) : int -> (fo_term int int))
                  identity identity))
               (identity) (identity)) ;
          model_equal_fo_term_list v1 subst_id_symbol
            (rename_subst_symbol
               ((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
            const (Var_symbol (-1)) : int -> (symbol int)))
            (rename_subst_symbol
               ((rename_subst_symbol
                  (const (Var_symbol (-1)) : int -> (symbol int)) identity))
               (identity))
            subst_id_fo_term
            (rename_subst_fo_term
               ((rename_subst_fo_term subst_id_fo_term identity identity))
               (identity) (identity)) ((const (Var_fo_term (-1)) :
                                          int -> (fo_term int int)))
            (rename_subst_fo_term
               ((rename_subst_fo_term
                  (const (Var_fo_term (-1)) : int -> (fo_term int int))
                  identity identity))
               (identity) (identity)) ;
          let ghost mrv0 = rename_fo_term mv0 identity identity in
          let ghost mrv1 = rename_fo_term_list mv1 identity identity in
          let resv0 =
            { nlrepr_fo_term_field = v0 ;
              nlfree_var_symbol_set_abstraction_fo_term_field = fv0 ;
              nlfree_var_fo_term_set_abstraction_fo_term_field = fv3 ;
              model_fo_term_field = ghost mrv0 ;
            }
          in
          let resv1 =
            { nlrepr_fo_term_list_field = v1 ;
              nlfree_var_symbol_set_abstraction_fo_term_list_field = fv0 ;
              nlfree_var_fo_term_set_abstraction_fo_term_list_field = fv3 ;
              model_fo_term_list_field = ghost mrv1 ;
            }
          in let res = NLC_FOCons resv0 resv1 in
          free_var_equivalence_of_rename_fo_term mv0 (identity)
            (rcompose (identity) (identity)) (identity)
            (rcompose (identity) (identity)) ;
          free_var_equivalence_of_rename_fo_term_list mv1 (identity)
            (rcompose (identity) (identity)) (identity)
            (rcompose (identity) (identity)) ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_term x mrv0 ->
              (forall y:int.
                 (is_symbol_free_var_in_fo_term y mv0 /\ eval (identity) y =
                    x)
                 -> x = y &&
                 is_symbol_free_var_in_fo_term_list x
                   t.model_fo_term_list_field
                 && (x) < (fv0))
              && (x) < (fv0)
            } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_term x mrv0 ->
              (forall y:int.
                 (is_fo_term_free_var_in_fo_term y mv0 /\ eval (identity) y =
                    x)
                 -> x = y &&
                 is_fo_term_free_var_in_fo_term_list x
                   t.model_fo_term_list_field
                 && (x) < (fv3))
              && (x) < (fv3)
            } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_term_list x mrv1 ->
              (forall y:int.
                 (is_symbol_free_var_in_fo_term_list y mv1 /\
                    eval (identity) y = x)
                 -> x = y &&
                 is_symbol_free_var_in_fo_term_list x
                   t.model_fo_term_list_field
                 && (x) < (fv0))
              && (x) < (fv0)
            } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_term_list x mrv1 ->
              (forall y:int.
                 (is_fo_term_free_var_in_fo_term_list y mv1 /\
                    eval (identity) y = x)
                 -> x = y &&
                 is_fo_term_free_var_in_fo_term_list x
                   t.model_fo_term_list_field
                 && (x) < (fv3))
              && (x) < (fv3)
            } ;
          res
    end

  let destruct_fo_term (t:nlimpl_fo_term) : cons_fo_term
    requires { nlimpl_fo_term_ok t } ensures { cons_ok_fo_term result }
    ensures { cons_rel_fo_term result t }
    ensures { cons_open_rel_fo_term result t } =
    let fv0 = t.nlfree_var_symbol_set_abstraction_fo_term_field in
    let fv3 = t.nlfree_var_fo_term_set_abstraction_fo_term_field in
    match t.nlrepr_fo_term_field with
      | NLFVar_fo_term v0 -> NLCVar_fo_term v0
      | NLBruijn_fo_term v0 -> absurd
      | NL_App v0 v1 ->
        assert { t.model_fo_term_field =
          App
            (nlmodel_symbol v0 (rename_subst_symbol subst_id_symbol identity)
               (rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity))
            (nlmodel_fo_term_list v1
               (rename_subst_symbol subst_id_symbol identity)
               (rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity)
               (rename_subst_fo_term subst_id_fo_term identity identity)
               (rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
          } ;
          let (mv0 , mv1) =
            match t.model_fo_term_field with | Var_fo_term x0 -> absurd
              | App x0 x1 -> (x0 , x1)
            end
          in
          assert { mv0 =
            nlmodel_symbol v0
              ((rename_subst_symbol subst_id_symbol identity))
              ((rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity))
            } ;
          assert { mv1 =
            nlmodel_fo_term_list v1
              ((rename_subst_symbol subst_id_symbol identity))
              ((rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity))
              ((rename_subst_fo_term subst_id_fo_term identity identity))
              ((rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
            } ;
          assert { bound_depth_of_symbol_in_symbol v0 <= 0 } ;
          assert {
            forall x:int. is_symbol_free_var_in_symbol x mv0 ->
              is_symbol_free_var_in_fo_term x t.model_fo_term_field && (x) <
              (t.nlfree_var_symbol_set_abstraction_fo_term_field)
            } ;
          assert { bound_depth_of_symbol_in_fo_term_list v1 <= 0 } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_term_list x mv1 ->
              is_symbol_free_var_in_fo_term x t.model_fo_term_field && (x) <
              (t.nlfree_var_symbol_set_abstraction_fo_term_field)
            } ;
          assert { bound_depth_of_fo_term_in_fo_term_list v1 <= 0 } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_term_list x mv1 ->
              is_fo_term_free_var_in_fo_term x t.model_fo_term_field && (x) <
              (t.nlfree_var_fo_term_set_abstraction_fo_term_field)
            } ;
          model_equal_symbol v0 subst_id_symbol
            (rename_subst_symbol
               ((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
            const (Var_symbol (-1)) : int -> (symbol int)))
            (rename_subst_symbol
               ((rename_subst_symbol
                  (const (Var_symbol (-1)) : int -> (symbol int)) identity))
               (identity)) ;
          model_equal_fo_term_list v1 subst_id_symbol
            (rename_subst_symbol
               ((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
            const (Var_symbol (-1)) : int -> (symbol int)))
            (rename_subst_symbol
               ((rename_subst_symbol
                  (const (Var_symbol (-1)) : int -> (symbol int)) identity))
               (identity))
            subst_id_fo_term
            (rename_subst_fo_term
               ((rename_subst_fo_term subst_id_fo_term identity identity))
               (identity) (identity)) ((const (Var_fo_term (-1)) :
                                          int -> (fo_term int int)))
            (rename_subst_fo_term
               ((rename_subst_fo_term
                  (const (Var_fo_term (-1)) : int -> (fo_term int int))
                  identity identity))
               (identity) (identity)) ;
          let ghost mrv0 = rename_symbol mv0 identity in
          let ghost mrv1 = rename_fo_term_list mv1 identity identity in
          let resv0 =
            { nlrepr_symbol_field = v0 ;
              nlfree_var_symbol_set_abstraction_symbol_field = fv0 ;
              model_symbol_field = ghost mrv0 ;
            }
          in
          let resv1 =
            { nlrepr_fo_term_list_field = v1 ;
              nlfree_var_symbol_set_abstraction_fo_term_list_field = fv0 ;
              nlfree_var_fo_term_set_abstraction_fo_term_list_field = fv3 ;
              model_fo_term_list_field = ghost mrv1 ;
            }
          in let res = NLC_App resv0 resv1 in
          free_var_equivalence_of_rename_symbol mv0 (identity)
            (rcompose (identity) (identity)) ;
          free_var_equivalence_of_rename_fo_term_list mv1 (identity)
            (rcompose (identity) (identity)) (identity)
            (rcompose (identity) (identity)) ;
          assert {
            forall x:int. is_symbol_free_var_in_symbol x mrv0 ->
              (forall y:int.
                 (is_symbol_free_var_in_symbol y mv0 /\ eval (identity) y = x)
                 -> x = y &&
                 is_symbol_free_var_in_fo_term x t.model_fo_term_field && (x)
                 < (fv0))
              && (x) < (fv0)
            } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_term_list x mrv1 ->
              (forall y:int.
                 (is_symbol_free_var_in_fo_term_list y mv1 /\
                    eval (identity) y = x)
                 -> x = y &&
                 is_symbol_free_var_in_fo_term x t.model_fo_term_field && (x)
                 < (fv0))
              && (x) < (fv0)
            } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_term_list x mrv1 ->
              (forall y:int.
                 (is_fo_term_free_var_in_fo_term_list y mv1 /\
                    eval (identity) y = x)
                 -> x = y &&
                 is_fo_term_free_var_in_fo_term x t.model_fo_term_field &&
                 (x) < (fv3))
              && (x) < (fv3)
            } ;
          res
    end

  let nlsubst_symbol_in_fo_term_list (t:nlimpl_fo_term_list) (x:int)
    (u:nlimpl_symbol) : nlimpl_fo_term_list
    requires { nlimpl_fo_term_list_ok t } requires { nlimpl_symbol_ok u }
    ensures { nlimpl_fo_term_list_ok result }
    ensures { result.model_fo_term_list_field =
      subst_fo_term_list t.model_fo_term_list_field
        (update (subst_id_symbol: (int) -> (symbol (int))) x
           u.model_symbol_field)
        (subst_id_fo_term: (int) -> (fo_term (int) (int)))
      }
    =
    model_equal_fo_term_list t.nlrepr_fo_term_list_field
      (subst_compose_symbol subst_id_symbol
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field)))
      ((update (subst_id_symbol: (int) -> (symbol (int))) x
          u.model_symbol_field))
      (subst_compose_symbol (const (Var_symbol (-1)))
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field)))
      ((const (Var_symbol (-1))))
      (subst_compose_fo_term subst_id_fo_term
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field))
         ((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
      ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
      (subst_compose_fo_term (const (Var_fo_term (-1)))
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field))
         ((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
      ((const (Var_fo_term (-1))));
    let res =
      {
        nlrepr_fo_term_list_field =
          subst_base_symbol_in_fo_term_list t.nlrepr_fo_term_list_field x
            u.nlrepr_symbol_field (subst_id_symbol)
            ((const (Var_symbol (-1)))) (subst_id_fo_term)
            ((const (Var_fo_term (-1)))) ((const (Var_symbol (-1)))) ;
        nlfree_var_symbol_set_abstraction_fo_term_list_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_symbol_set_abstraction_fo_term_list_field)
               (u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
        nlfree_var_fo_term_set_abstraction_fo_term_list_field =
          t.nlfree_var_fo_term_set_abstraction_fo_term_list_field ;
        model_fo_term_list_field = ghost
          subst_fo_term_list t.model_fo_term_list_field
            (update (subst_id_symbol: (int) -> (symbol (int))) x
               u.model_symbol_field)
            (subst_id_fo_term: (int) -> (fo_term (int) (int))) ;
      }
    in
    assert {
      forall x2:int.
        is_symbol_free_var_in_fo_term_list x2 res.model_fo_term_list_field ->
        (true /\
           (forall y:int.
              (is_symbol_free_var_in_fo_term_list y
                 t.model_fo_term_list_field /\
                 is_symbol_free_var_in_symbol x2
                   (eval
                      ((update (subst_id_symbol: (int) -> (symbol (int))) x
                          u.model_symbol_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_symbol_set_abstraction_fo_term_list_field))
                 /\
                 (x <> y -> x2 = y && (x2) <
                    (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)))
                 && (x2) <
                 (res.nlfree_var_symbol_set_abstraction_fo_term_list_field))
           /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term_list y
                 t.model_fo_term_list_field /\
                 is_symbol_free_var_in_fo_term x2
                   (eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
                      y))
              -> false))
        && (x2) < (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
      } ;
    assert {
      forall x2:int.
        is_fo_term_free_var_in_fo_term_list x2 res.model_fo_term_list_field
        ->
        (true /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term_list y
                 t.model_fo_term_list_field /\
                 is_fo_term_free_var_in_fo_term x2
                   (eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
                      y))
              -> x2 = y && (x2) <
              (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)))
        && (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
      } ;
    res

  let nlsubst_fo_term_in_fo_term_list (t:nlimpl_fo_term_list) (x:int)
    (u:nlimpl_fo_term) : nlimpl_fo_term_list
    requires { nlimpl_fo_term_list_ok t } requires { nlimpl_fo_term_ok u }
    ensures { nlimpl_fo_term_list_ok result }
    ensures { result.model_fo_term_list_field =
      subst_fo_term_list t.model_fo_term_list_field
        (subst_id_symbol: (int) -> (symbol (int)))
        (update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
           u.model_fo_term_field)
      }
    =
    model_equal_fo_term_list t.nlrepr_fo_term_list_field
      (subst_compose_symbol subst_id_symbol
         ((subst_id_symbol: (int) -> (symbol (int)))))
      ((subst_id_symbol: (int) -> (symbol (int))))
      (subst_compose_symbol (const (Var_symbol (-1)))
         ((subst_id_symbol: (int) -> (symbol (int)))))
      ((const (Var_symbol (-1))))
      (subst_compose_fo_term subst_id_fo_term
         ((subst_id_symbol: (int) -> (symbol (int))))
         ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
             u.model_fo_term_field)))
      ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
          u.model_fo_term_field))
      (subst_compose_fo_term (const (Var_fo_term (-1)))
         ((subst_id_symbol: (int) -> (symbol (int))))
         ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
             u.model_fo_term_field)))
      ((const (Var_fo_term (-1))));
    let res =
      {
        nlrepr_fo_term_list_field =
          subst_base_fo_term_in_fo_term_list t.nlrepr_fo_term_list_field x
            u.nlrepr_fo_term_field (subst_id_symbol)
            ((const (Var_symbol (-1)))) (subst_id_fo_term)
            ((const (Var_fo_term (-1)))) ((const (Var_symbol (-1))))
            ((const (Var_fo_term (-1)))) ;
        nlfree_var_symbol_set_abstraction_fo_term_list_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_symbol_set_abstraction_fo_term_list_field)
               (u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
        nlfree_var_fo_term_set_abstraction_fo_term_list_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
               (u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
        model_fo_term_list_field = ghost
          subst_fo_term_list t.model_fo_term_list_field
            (subst_id_symbol: (int) -> (symbol (int)))
            (update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
               u.model_fo_term_field) ;
      }
    in
    assert {
      forall x2:int.
        is_symbol_free_var_in_fo_term_list x2 res.model_fo_term_list_field ->
        (true /\
           (forall y:int.
              (is_symbol_free_var_in_fo_term_list y
                 t.model_fo_term_list_field /\
                 is_symbol_free_var_in_symbol x2
                   (eval ((subst_id_symbol: (int) -> (symbol (int)))) y))
              -> x2 = y && (x2) <
              (res.nlfree_var_symbol_set_abstraction_fo_term_list_field))
           /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term_list y
                 t.model_fo_term_list_field /\
                 is_symbol_free_var_in_fo_term x2
                   (eval
                      ((update
                          (subst_id_fo_term: (int) -> (fo_term (int) (int)))
                          x u.model_fo_term_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_symbol_set_abstraction_fo_term_list_field))
                 /\ (x <> y -> false)) && (x2) <
                 (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)))
        && (x2) < (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
      } ;
    assert {
      forall x2:int.
        is_fo_term_free_var_in_fo_term_list x2 res.model_fo_term_list_field
        ->
        (true /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term_list y
                 t.model_fo_term_list_field /\
                 is_fo_term_free_var_in_fo_term x2
                   (eval
                      ((update
                          (subst_id_fo_term: (int) -> (fo_term (int) (int)))
                          x u.model_fo_term_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field))
                 /\
                 (x <> y -> x2 = y && (x2) <
                    (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)))
                 && (x2) <
                 (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)))
        && (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
      } ;
    res

  let nlsubst_symbol_in_fo_term (t:nlimpl_fo_term) (x:int)
    (u:nlimpl_symbol) : nlimpl_fo_term requires { nlimpl_fo_term_ok t }
    requires { nlimpl_symbol_ok u } ensures { nlimpl_fo_term_ok result }
    ensures { result.model_fo_term_field =
      subst_fo_term t.model_fo_term_field
        (update (subst_id_symbol: (int) -> (symbol (int))) x
           u.model_symbol_field)
        (subst_id_fo_term: (int) -> (fo_term (int) (int)))
      }
    =
    model_equal_fo_term t.nlrepr_fo_term_field
      (subst_compose_symbol subst_id_symbol
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field)))
      ((update (subst_id_symbol: (int) -> (symbol (int))) x
          u.model_symbol_field))
      (subst_compose_symbol (const (Var_symbol (-1)))
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field)))
      ((const (Var_symbol (-1))))
      (subst_compose_fo_term subst_id_fo_term
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field))
         ((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
      ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
      (subst_compose_fo_term (const (Var_fo_term (-1)))
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field))
         ((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
      ((const (Var_fo_term (-1))));
    let res =
      {
        nlrepr_fo_term_field =
          subst_base_symbol_in_fo_term t.nlrepr_fo_term_field x
            u.nlrepr_symbol_field (subst_id_symbol)
            ((const (Var_symbol (-1)))) (subst_id_fo_term)
            ((const (Var_fo_term (-1)))) ((const (Var_symbol (-1)))) ;
        nlfree_var_symbol_set_abstraction_fo_term_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_symbol_set_abstraction_fo_term_field)
               (u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
        nlfree_var_fo_term_set_abstraction_fo_term_field =
          t.nlfree_var_fo_term_set_abstraction_fo_term_field ;
        model_fo_term_field = ghost
          subst_fo_term t.model_fo_term_field
            (update (subst_id_symbol: (int) -> (symbol (int))) x
               u.model_symbol_field)
            (subst_id_fo_term: (int) -> (fo_term (int) (int))) ;
      }
    in
    assert {
      forall x2:int. is_symbol_free_var_in_fo_term x2 res.model_fo_term_field
        ->
        (true /\
           (forall y:int.
              (is_symbol_free_var_in_fo_term y t.model_fo_term_field /\
                 is_symbol_free_var_in_symbol x2
                   (eval
                      ((update (subst_id_symbol: (int) -> (symbol (int))) x
                          u.model_symbol_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_symbol_set_abstraction_fo_term_field))
                 /\
                 (x <> y -> x2 = y && (x2) <
                    (res.nlfree_var_symbol_set_abstraction_fo_term_field)))
                 && (x2) <
                 (res.nlfree_var_symbol_set_abstraction_fo_term_field))
           /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term y t.model_fo_term_field /\
                 is_symbol_free_var_in_fo_term x2
                   (eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
                      y))
              -> false))
        && (x2) < (res.nlfree_var_symbol_set_abstraction_fo_term_field)
      } ;
    assert {
      forall x2:int.
        is_fo_term_free_var_in_fo_term x2 res.model_fo_term_field ->
        (true /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term y t.model_fo_term_field /\
                 is_fo_term_free_var_in_fo_term x2
                   (eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
                      y))
              -> x2 = y && (x2) <
              (res.nlfree_var_fo_term_set_abstraction_fo_term_field)))
        && (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_field)
      } ;
    res

  let nlsubst_fo_term_in_fo_term (t:nlimpl_fo_term) (x:int)
    (u:nlimpl_fo_term) : nlimpl_fo_term requires { nlimpl_fo_term_ok t }
    requires { nlimpl_fo_term_ok u } ensures { nlimpl_fo_term_ok result }
    ensures { result.model_fo_term_field =
      subst_fo_term t.model_fo_term_field
        (subst_id_symbol: (int) -> (symbol (int)))
        (update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
           u.model_fo_term_field)
      }
    =
    model_equal_fo_term t.nlrepr_fo_term_field
      (subst_compose_symbol subst_id_symbol
         ((subst_id_symbol: (int) -> (symbol (int)))))
      ((subst_id_symbol: (int) -> (symbol (int))))
      (subst_compose_symbol (const (Var_symbol (-1)))
         ((subst_id_symbol: (int) -> (symbol (int)))))
      ((const (Var_symbol (-1))))
      (subst_compose_fo_term subst_id_fo_term
         ((subst_id_symbol: (int) -> (symbol (int))))
         ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
             u.model_fo_term_field)))
      ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
          u.model_fo_term_field))
      (subst_compose_fo_term (const (Var_fo_term (-1)))
         ((subst_id_symbol: (int) -> (symbol (int))))
         ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
             u.model_fo_term_field)))
      ((const (Var_fo_term (-1))));
    let res =
      {
        nlrepr_fo_term_field =
          subst_base_fo_term_in_fo_term t.nlrepr_fo_term_field x
            u.nlrepr_fo_term_field (subst_id_symbol)
            ((const (Var_symbol (-1)))) (subst_id_fo_term)
            ((const (Var_fo_term (-1)))) ((const (Var_symbol (-1))))
            ((const (Var_fo_term (-1)))) ;
        nlfree_var_symbol_set_abstraction_fo_term_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_symbol_set_abstraction_fo_term_field)
               (u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
        nlfree_var_fo_term_set_abstraction_fo_term_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_fo_term_set_abstraction_fo_term_field)
               (u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
        model_fo_term_field = ghost
          subst_fo_term t.model_fo_term_field
            (subst_id_symbol: (int) -> (symbol (int)))
            (update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
               u.model_fo_term_field) ;
      }
    in
    assert {
      forall x2:int. is_symbol_free_var_in_fo_term x2 res.model_fo_term_field
        ->
        (true /\
           (forall y:int.
              (is_symbol_free_var_in_fo_term y t.model_fo_term_field /\
                 is_symbol_free_var_in_symbol x2
                   (eval ((subst_id_symbol: (int) -> (symbol (int)))) y))
              -> x2 = y && (x2) <
              (res.nlfree_var_symbol_set_abstraction_fo_term_field))
           /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term y t.model_fo_term_field /\
                 is_symbol_free_var_in_fo_term x2
                   (eval
                      ((update
                          (subst_id_fo_term: (int) -> (fo_term (int) (int)))
                          x u.model_fo_term_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_symbol_set_abstraction_fo_term_field))
                 /\ (x <> y -> false)) && (x2) <
                 (res.nlfree_var_symbol_set_abstraction_fo_term_field)))
        && (x2) < (res.nlfree_var_symbol_set_abstraction_fo_term_field)
      } ;
    assert {
      forall x2:int.
        is_fo_term_free_var_in_fo_term x2 res.model_fo_term_field ->
        (true /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_term y t.model_fo_term_field /\
                 is_fo_term_free_var_in_fo_term x2
                   (eval
                      ((update
                          (subst_id_fo_term: (int) -> (fo_term (int) (int)))
                          x u.model_fo_term_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_fo_term_set_abstraction_fo_term_field))
                 /\
                 (x <> y -> x2 = y && (x2) <
                    (res.nlfree_var_fo_term_set_abstraction_fo_term_field)))
                 && (x2) <
                 (res.nlfree_var_fo_term_set_abstraction_fo_term_field)))
        && (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_field)
      } ;
    res

end