Step * of Lemma accum_filter_rel_nil

[T,A:Type]. ∀[a,b:A]. ∀[P,f:Top].  uiff(b accum(z,x.f[z;x],a,{x∈[]|P[x]});b a ∈ A)
BY
RepeatFor ((D THENA (Auto THEN AutoSimpHyp Auto (-1)))) }

1
1. Type
2. Type
3. A
4. A
5. Top
6. Top
7. accum(z,x.f[z;x],a,{x∈[]|P[x]})
⊢ a ∈ A

2
1. Type
2. Type
3. A
4. A
5. Top
6. Top
7. a ∈ A
⊢ accum(z,x.f[z;x],a,{x∈[]|P[x]})


Latex:


Latex:
\mforall{}[T,A:Type].  \mforall{}[a,b:A].  \mforall{}[P,f:Top].    uiff(b  =  accum(z,x.f[z;x],a,\{x\mmember{}[]|P[x]\});b  =  a)


By


Latex:
RepeatFor  8  ((D  0  THENA  (Auto  THEN  AutoSimpHyp  Auto  (-1))))




Home Index