3 begin

     3 begin

     4 

     4 

     5 (* core haskell *)

     5 (* core haskell *)

     6 

     6 

     7 ML {* val _ = recursive := false *}

     7 ML {* val _ = recursive := false *}

     8 

    11 

     9 atom_decl var

    12 atom_decl var

    10 atom_decl cvar

    13 atom_decl cvar

    11 atom_decl tvar

    14 atom_decl tvar

    12 

    15 

    85 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t"

    88 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t"

    86 | "bv_tvs TvsNil = []"

    89 | "bv_tvs TvsNil = []"

    87 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"

    90 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"

    88 | "bv_cvs CvsNil = []"

    91 | "bv_cvs CvsNil = []"

    89 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"

    92 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"

    90 

    94 

    91 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)

    95 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)

    92 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]

    96 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]

    93 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

    97 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

    94 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff

    98 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff