---

Step * 1 of Lemma Wcmp_wf


1. A : Type
2. B : A ⟶ Type
3. leq : 𝔹
4. x : W(A;a.B[a])
5. y : W(A;a.B[a])
⊢ Wcmp(A;a.B[a];leq) x y ∈ ℙ
BY
{ (MoveToConcl (-3)
   THEN MoveToConcl (-1)
   THEN WElim (-1)
   THEN (D 0 THENA Auto)
   THEN WElim (-1)
   THEN Auto
   THEN RecUnfold `Wcmp` 0
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  leq  :  \mBbbB{}
4.  x  :  W(A;a.B[a])
5.  y  :  W(A;a.B[a])
\mvdash{}  Wcmp(A;a.B[a];leq)  x  y  \mmember{}  \mBbbP{}


By

---

Latex:
(MoveToConcl  (-3)
  THEN  MoveToConcl  (-1)
  THEN  WElim  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  WElim  (-1)
  THEN  Auto
  THEN  RecUnfold  `Wcmp`  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index