equal
deleted
inserted
replaced
180 "[| equiv A r; congruent r b; X: A/r; \ |
180 "[| equiv A r; congruent r b; X: A/r; \ |
181 \ !!x. x : A ==> b(x) : B |] \ |
181 \ !!x. x : A ==> b(x) : B |] \ |
182 \ ==> (UN x:X. b(x)) : B"; |
182 \ ==> (UN x:X. b(x)) : B"; |
183 by (cut_facts_tac prems 1); |
183 by (cut_facts_tac prems 1); |
184 by (safe_tac (!claset)); |
184 by (safe_tac (!claset)); |
185 by (rtac (localize UN_equiv_class RS ssubst) 1); |
185 by (stac (localize UN_equiv_class) 1); |
186 by (REPEAT (ares_tac prems 1)); |
186 by (REPEAT (ares_tac prems 1)); |
187 qed "UN_equiv_class_type"; |
187 qed "UN_equiv_class_type"; |
188 |
188 |
189 (*Sufficient conditions for injectiveness. Could weaken premises! |
189 (*Sufficient conditions for injectiveness. Could weaken premises! |
190 major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B |
190 major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B |