equal
deleted
inserted
replaced
6 |
6 |
7 atom_decl var |
7 atom_decl var |
8 atom_decl cvar |
8 atom_decl cvar |
9 atom_decl tvar |
9 atom_decl tvar |
10 |
10 |
11 declare [[STEPS = 15]] |
11 declare [[STEPS = 16]] |
12 |
12 |
13 nominal_datatype tkind = |
13 nominal_datatype tkind = |
14 KStar |
14 KStar |
15 | KFun "tkind" "tkind" |
15 | KFun "tkind" "tkind" |
16 and ckind = |
16 and ckind = |
82 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
82 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
83 | "bv_tvs TvsNil = []" |
83 | "bv_tvs TvsNil = []" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_cvs CvsNil = []" |
85 | "bv_cvs CvsNil = []" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
|
87 |
|
88 |
|
89 term TvsNil |
|
90 |
87 |
91 |
88 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 fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
93 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
94 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
91 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
95 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |