src/ZF/AC/AC7_AC9.ML
changeset 5470 855654b691db
parent 5325 f7a5e06adea1
child 9683 f87c8c449018
equal deleted inserted replaced
5469:024d887eae50 5470:855654b691db
    89 Goal "y: (PROD B:{Y*C. C:A}. B) ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
    89 Goal "y: (PROD B:{Y*C. C:A}. B) ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
    90 by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
    90 by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
    91 val lemma1_2 = result();
    91 val lemma1_2 = result();
    92 
    92 
    93 Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0";
    93 Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0";
    94 by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]
    94 by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1);
    95                 addSEs [equals0E]) 1);
       
    96 val lemma1 = result();
    95 val lemma1 = result();
    97 
    96 
    98 Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
    97 Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
    99 by (fast_tac (claset() addEs [Sigma_fun_space_not0 RS not_sym RS notE]) 1);
    98 by (fast_tac (claset() addEs [Sigma_fun_space_not0 RS not_sym RS notE]) 1);
   100 val lemma2 = result();
    99 val lemma2 = result();