---

Step * of Lemma WtoSet-order-preserving

∀[A:Type]. ∀[B:A ⟶ Type].
  ∀x,y:W(A;a.B[a]). ∀b:𝔹.  ((x Wcmp(A;a.B[a];b) y) ⇒ (WtoSet(a.B[a];x) Wcmp(Type;a.a;b) WtoSet(a.B[a];y)))
BY
{ (RepeatFor 2 (Intro)
   THEN RepeatFor 2 (UseWInductionLemma')
   THEN RepeatFor 2 ((D 0 THENA (Auto THEN UsingVars [`A'] MemCD⋅ THEN Auto)))
   THEN Unfold `WtoSet` 0
   THEN RepUR ``Wsup`` 0
   THEN RecUnfold `Wcmp` (-1)
   THEN Reduce -1
   THEN RecUnfold `Wcmp` 0
   THEN Reduce 0
   THEN D -2
   THEN All Reduce
   THEN ParallelLast) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W(A;a.B[a])
5. ∀b:B[a]. ∀y:W(A;a.B[a]). ∀b@0:𝔹.
     (((f b) Wcmp(A;a.B[a];b@0) y) ⇒ (WtoSet(a.B[a];f b) Wcmp(Type;a.a;b@0) WtoSet(a.B[a];y)))
6. a@0 : A
7. f@0 : B[a@0] ⟶ W(A;a.B[a])
8. ∀b:B[a@0]. ∀b@0:𝔹.
     ((Wsup(a;f) Wcmp(A;a.B[a];b@0) (f@0 b)) ⇒ (WtoSet(a.B[a];Wsup(a;f)) Wcmp(Type;a.a;b@0) WtoSet(a.B[a];f@0 b)))
9. x : Unit
10. ∀x:B[a]. ((f x) <  Wsup(a@0;f@0))
11. x1 : B[a]
12. (f x1) <  Wsup(a@0;f@0)
⊢ WtoSet(a.B[a];f x1) <  λb.WtoSet(a.B[a];f@0 b)"(B[a@0])

2
1. [A] : Type
2. [B] : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W(A;a.B[a])
5. ∀b:B[a]. ∀y:W(A;a.B[a]). ∀b@0:𝔹.
     (((f b) Wcmp(A;a.B[a];b@0) y) ⇒ (WtoSet(a.B[a];f b) Wcmp(Type;a.a;b@0) WtoSet(a.B[a];y)))
6. a@0 : A
7. f@0 : B[a@0] ⟶ W(A;a.B[a])
8. ∀b:B[a@0]. ∀b@0:𝔹.
     ((Wsup(a;f) Wcmp(A;a.B[a];b@0) (f@0 b)) ⇒ (WtoSet(a.B[a];Wsup(a;f)) Wcmp(Type;a.a;b@0) WtoSet(a.B[a];f@0 b)))
9. y : Unit
10. x : B[a@0]
11. Wsup(a;f) ≤  (f@0 x)
⊢ λb.WtoSet(a.B[a];f b)"(B[a]) ≤  WtoSet(a.B[a];f@0 x)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}x,y:W(A;a.B[a]).  \mforall{}b:\mBbbB{}.
        ((x  Wcmp(A;a.B[a];b)  y)  {}\mRightarrow{}  (WtoSet(a.B[a];x)  Wcmp(Type;a.a;b)  WtoSet(a.B[a];y)))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  RepeatFor  2  (UseWInductionLemma')
  THEN  RepeatFor  2  ((D  0  THENA  (Auto  THEN  UsingVars  [`A']  MemCD\mcdot{}  THEN  Auto)))
  THEN  Unfold  `WtoSet`  0
  THEN  RepUR  ``Wsup``  0
  THEN  RecUnfold  `Wcmp`  (-1)
  THEN  Reduce  -1
  THEN  RecUnfold  `Wcmp`  0
  THEN  Reduce  0
  THEN  D  -2
  THEN  All  Reduce
  THEN  ParallelLast)

---

Home Index