alias symbol "covers" = "covers".
alias symbol "covers" = "covers set".
alias symbol "covers" = "covers".
alias symbol "covers" = "covers".
alias symbol "covers" = "covers set".
alias symbol "covers" = "covers".
nlemma cover_ind'':
∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
(∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
nlemma cover_ind'':
∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
(∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
nrewrite > E2; nnormalize; #_; nauto]##]
#Hcut;
nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
nrewrite > E2; nnormalize; #_; nauto]##]
#Hcut;
nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;