---

Step * of Lemma discrete-family_wf

No Annotations
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[X:j⊢].  X.discr(A) ⊢ discrete-family(A;a.B[a])
BY
{ (Intros
   THEN MemTypeCD
   THEN Try ((Unfold `discrete-family` 0
              THEN RepUR ``cube-context-adjoin discrete-cubical-type`` 0
              THEN (Complete (Auto) ORELSE (MemCD THEN Reduce 0 THEN Complete (Auto)))))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[X:j\mvdash{}].    X.discr(A)  \mvdash{}  discrete-family(A;a.B[a])


By

---

Latex:
(Intros
  THEN  MemTypeCD
  THEN  Try  ((Unfold  `discrete-family`  0
                        THEN  RepUR  ``cube-context-adjoin  discrete-cubical-type``  0
                        THEN  (Complete  (Auto)  ORELSE  (MemCD  THEN  Reduce  0  THEN  Complete  (Auto)))))
  THEN  Auto)

---

Home Index