---

Step * of Lemma per-or_wf

∀[A,B:Type].  (per-or(A;B) ∈ Type)
BY
{ TACTIC:(Auto
          THEN Unfold `per-or` 0
          THEN (InstLemma `per-exists_wf` [⌜per-value()⌝]⋅ THENA Auto)
          THEN BHyp (-1)
          THEN Fold `per-or-family` 0
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (per-or(A;B)  \mmember{}  Type)


By

---

Latex:
TACTIC:(Auto
                THEN  Unfold  `per-or`  0
                THEN  (InstLemma  `per-exists\_wf`  [\mkleeneopen{}per-value()\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  BHyp  (-1)
                THEN  Fold  `per-or-family`  0
                THEN  Auto)

---

Home Index