148 lemmas csubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] |
148 lemmas csubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] |
149 lemmas csubset_eq[no_atp] = subset_eq[Transfer.transferred] |
149 lemmas csubset_eq[no_atp] = subset_eq[Transfer.transferred] |
150 lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred] |
150 lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred] |
151 lemmas csubset_refl = subset_refl[Transfer.transferred] |
151 lemmas csubset_refl = subset_refl[Transfer.transferred] |
152 lemmas csubset_trans = subset_trans[Transfer.transferred] |
152 lemmas csubset_trans = subset_trans[Transfer.transferred] |
153 lemmas cset_rev_mp = set_rev_mp[Transfer.transferred] |
153 lemmas cset_rev_mp = rev_subsetD[Transfer.transferred] |
154 lemmas cset_mp = set_mp[Transfer.transferred] |
154 lemmas cset_mp = subsetD[Transfer.transferred] |
155 lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] |
155 lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] |
156 lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred] |
156 lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred] |
157 lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred] |
157 lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred] |
158 lemmas cequalityD1 = equalityD1[Transfer.transferred] |
158 lemmas cequalityD1 = equalityD1[Transfer.transferred] |
159 lemmas cequalityD2 = equalityD2[Transfer.transferred] |
159 lemmas cequalityD2 = equalityD2[Transfer.transferred] |