equal
deleted
inserted
replaced
14 inductive |
14 inductive |
15 domains "Fin(A)" <= "Pow(A)" |
15 domains "Fin(A)" <= "Pow(A)" |
16 intrs |
16 intrs |
17 emptyI "0 : Fin(A)" |
17 emptyI "0 : Fin(A)" |
18 consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" |
18 consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" |
19 type_intrs "[empty_subsetI, cons_subsetI, PowI]" |
19 type_intrs empty_subsetI, cons_subsetI, PowI |
20 type_elims "[make_elim PowD]" |
20 type_elims "[make_elim PowD]" |
21 |
21 |
22 inductive |
22 inductive |
23 domains "FiniteFun(A,B)" <= "Fin(A*B)" |
23 domains "FiniteFun(A,B)" <= "Fin(A*B)" |
24 intrs |
24 intrs |