---

Step * of Lemma W-rec_wf

∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[F:a:A ⟶ (B[a] ⟶ W(A;a.B[a])) ⟶ (B[a] ⟶ T) ⟶ T]. ∀[w:W(A;a.B[a])].
  (W-rec(a,f,r.F[a;f;r];w) ∈ T)
BY
{ (Auto THEN WElim (-1)) }

1
1. T : Type
2. A : Type
3. B : A ⟶ Type
4. F : a:A ⟶ (B[a] ⟶ W(A;a.B[a])) ⟶ (B[a] ⟶ T) ⟶ T
5. a : A
6. f : B[a] ⟶ W(A;a.B[a])
7. ∀b:B[a]. (W-rec(a,f,r.F[a;f;r];f b) ∈ T)
⊢ W-rec(a,f,r.F[a;f;r];Wsup(a;f)) ∈ T

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[F:a:A  {}\mrightarrow{}  (B[a]  {}\mrightarrow{}  W(A;a.B[a]))  {}\mrightarrow{}  (B[a]  {}\mrightarrow{}  T)  {}\mrightarrow{}  T].
\mforall{}[w:W(A;a.B[a])].
    (W-rec(a,f,r.F[a;f;r];w)  \mmember{}  T)


By

---

Latex:
(Auto  THEN  WElim  (-1))

---

Home Index