equal
deleted
inserted
replaced
82 | "bv_vs VsNil = []" |
82 | "bv_vs VsNil = []" |
83 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
83 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
84 | "bv_tvs TvsNil = []" |
84 | "bv_tvs TvsNil = []" |
85 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
86 | "bv_cvs CvsNil = []" |
86 | "bv_cvs CvsNil = []" |
87 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
87 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
|
88 |
|
89 |
88 |
90 |
89 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
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) |
90 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
92 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
91 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
93 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
92 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
94 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |