---

Step * of Lemma decidable__per-quotient_equal

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E[x;y]) ⇒ (∀x,y:T.  Dec(E[x;y])) ⇒ (∀u,v:x,y:T/per/E[x;y].  Dec(u = v ∈ (x,y:T/per/E[x;y]))))
BY
{ TACTIC:(TACTIC:InstLemma `decidable__quotient_equal` [] THEN NthHypSq (-1) THEN EqCD THEN Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(T;x,y.E[x;y])  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(E[x;y]))  {}\mRightarrow{}  (\mforall{}u,v:x,y:T/per/E[x;y].    Dec(u  =  v)))


By

---

Latex:
TACTIC:(TACTIC:InstLemma  `decidable\_\_quotient\_equal`  []
                THEN  NthHypSq  (-1)
                THEN  EqCD
                THEN  Auto
                THEN  Computation)

---

Home Index