- | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
- ]
- and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → b ∈ P ≝
- match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → b ∈ P with
- [ iter VV f ⇒ λb.λr. aux b (f b r) ]
+ | infinity a j q ⇒
+ H2 a j q
+ match q return λ_:(C ? a j) ◃ U.∀b. b ∈ (C ? a j) → b ∈ P with
+ [ iter f ⇒ λb.λr. aux b (f b r) ]]