---

Step * 1 1 of Lemma mk_deq_wf


1. T : Type
2. p : ∀x,y:T.  Dec(x = y ∈ T)
⊢ ∀x,y:T.  (x = y ∈ T ⇐⇒ ↑isl(p x y))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN  (GenConcl ⌜(p x y) = d ∈ Dec(x = y ∈ T)⌝⋅ THENA Auto)⋅
          THEN D -2
          THEN Reduce 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  \mforall{}x,y:T.    Dec(x  =  y)
\mvdash{}  \mforall{}x,y:T.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(p  x  y))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN    (GenConcl  \mkleeneopen{}(p  x  y)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}
                THEN  D  -2
                THEN  Reduce  0
                THEN  Auto)

---

Home Index