---

Step * of Lemma Wcmp_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[leq:𝔹].  (Wcmp(A;a.B[a];leq) ∈ W(A;a.B[a]) ⟶ W(A;a.B[a]) ⟶ ℙ)
BY
{ (Auto
   THEN (BetterExt THEN Try (Complete (Auto)))
   THEN (UnivCD THENA Auto)
   THEN ExtWith [`y'] [⌜Void ⟶ Void⌝]⋅
   THEN Try (Complete (Auto))) }

1
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 ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[leq:\mBbbB{}].    (Wcmp(A;a.B[a];leq)  \mmember{}  W(A;a.B[a])  {}\mrightarrow{}  W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  (BetterExt  THEN  Try  (Complete  (Auto)))
  THEN  (UnivCD  THENA  Auto)
  THEN  ExtWith  [`y']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index