C: βa:S. I a β Ξ© ^ S
}.
-notation "π term 90 a" non associative with precedence 70 for @{ 'I $a }.
-notation "π term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
+notation "π \sub( β¨term 90 aβ© )" non associative with precedence 70 for @{ 'I $a }.
+notation "π \sub ( β¨term 90 a,\emsp term 90 iβ© )" non associative with precedence 70 for @{ 'C $a $i }.
+
+notation > "π term 90 a" non associative with precedence 70 for @{ 'I $a }.
+notation > "π term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
interpretation "I" 'I a = (I ? a).
interpretation "C" 'C a i = (C ? a i).
ninductive cover (A : axiom_set) (U : Ξ©^A) : A β CProp[0] β
| creflexivity : βa:A. a β U β cover ? U a
-| cinfinity : βa:A. βi:?. ((C ? a i) β U) β cover ? U a.
+| cinfinity : βa:A.βi:π a. π a i β U β cover ? U a.
napply cover;
nqed.
interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
ncoinductive fish (A : axiom_set) (F : Ξ©^A) : A β CProp[0] β
-| cfish : βa. a β F β (βi:π a.C A a i β F) β fish A F a.
+| cfish : βa. a β F β (βi:π a .π a i β F) β fish A F a.
napply fish;
nqed.
nlet corec fish_rec (A:axiom_set) (U: Ξ©^A)
(P: Ξ©^A) (H1: P β U)
- (H2: βa:A. a β P β βj: π a. C ? a j β¬ P):
+ (H2: βa:A. a β P β βj: π a. π a j β¬ P):
βa:A. βp: a β P. a β U β ?.
#a; #p; napply cfish;
##[ napply H1; napply p;
##]
nqed.
-ntheorem coverage_min_cover_equation : βA,U,W. cover_equation A U W β βU β W.
+ntheorem coverage_min_cover_equation :
+ βA,U,W. cover_equation A U W β βU β W.
#A; #U; #W; #H; #a; #aU; nelim aU; #b;
##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;