---

Step * of Lemma discrete-path-equal

No Annotations
∀[T:Type]. ∀[X:j⊢]. ∀[a,b:{X ⊢ _:discr(T)}]. ∀[p1,p2:{X ⊢ _:(Path_discr(T) a b)}].
  (p1 = p2 ∈ {X ⊢ _:(Path_discr(T) a b)})
BY
{ (InstLemma `discrete-path` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Intros
   THEN (InstHyp [⌜p1⌝] (-3)⋅ THENA Auto)
   THEN (InstHyp [⌜p2⌝] (-4)⋅ THENA Auto)
   THEN Eq) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[a,b:\{X  \mvdash{}  \_:discr(T)\}].  \mforall{}[p1,p2:\{X  \mvdash{}  \_:(Path\_discr(T)  a  b)\}].    (p1  =  p2)


By

---

Latex:
(InstLemma  `discrete-path`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Intros
  THEN  (InstHyp  [\mkleeneopen{}p1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}p2\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  Eq)

---

Home Index