---

Step * 2 of Lemma dl-prop-deq_wf


1. x : Prop
2. y : Prop
3. ↑((λa,b. dlo_eq(prop(a);prop(b))) x y)
⊢ x = y ∈ Prop
BY
{ (Reduce -1 THEN RWO "assert-dlo_eq" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Prop
2.  y  :  Prop
3.  \muparrow{}((\mlambda{}a,b.  dlo\_eq(prop(a);prop(b)))  x  y)
\mvdash{}  x  =  y


By

---

Latex:
(Reduce  -1  THEN  RWO  "assert-dlo\_eq"  (-1)  THEN  Auto)

---

Home Index