---

Step * of Lemma W-sup_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[f:B[a] ⟶ W-type(A; a.B[a])].  (W-sup(a;f) ∈ W-type(A; a.B[a]))
BY
{ (Auto
   THEN MemTypeCD
   THEN Auto
   THEN Try ((co_WD 0 THEN ProveWfLemma))
   THEN (Assert W-sup(a;f) ∈ co-W(A;a.B[a]) BY
               (co_WD 0 THEN ProveWfLemma))
   THEN (Decide ⌜↑isl(p 0 a)⌝⋅ THENA Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. ↑isl(p 0 a)
⊢ W-bars(W-sup(a;f);p)

2
1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. ¬↑isl(p 0 a)
⊢ W-bars(W-sup(a;f);p)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[a:A].  \mforall{}[f:B[a]  {}\mrightarrow{}  W-type(A;  a.B[a])].    (W-sup(a;f)  \mmember{}  W-type(A;  a.B[a]))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((co\_WD  0  THEN  ProveWfLemma))
  THEN  (Assert  W-sup(a;f)  \mmember{}  co-W(A;a.B[a])  BY
                          (co\_WD  0  THEN  ProveWfLemma))
  THEN  (Decide  \mkleeneopen{}\muparrow{}isl(p  0  a)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index