---

Step * of Lemma per-eq-def_wf

∀[Term:Type]. ∀[EQ:Term ⟶ Term ⟶ Term ⟶ Term]. ∀[ts:candidate-type-system{i:l, i':l}(Term)]. ∀[T,T':Term].
∀[eq:term-equality{i:l}(Term)].
  per-eq-def{i:l}(Term;EQ;ts;T;T';eq) ∈ 𝕌' supposing Term ⊆r Base
BY
{ ((RepeatFor 2 (Intro) THEN (At ⌜𝕌{i''}⌝ Intro⋅ THEN Try (Complete ((MemCD THEN Auto)))) THEN Intros)
   THEN Unfold `per-eq-def` 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Term:Type].  \mforall{}[EQ:Term  {}\mrightarrow{}  Term  {}\mrightarrow{}  Term  {}\mrightarrow{}  Term].  \mforall{}[ts:candidate-type-system\{i:l,  i':l\}(Term)].
\mforall{}[T,T':Term].  \mforall{}[eq:term-equality\{i:l\}(Term)].
    per-eq-def\{i:l\}(Term;EQ;ts;T;T';eq)  \mmember{}  \mBbbU{}'  supposing  Term  \msubseteq{}r  Base


By

---

Latex:
((RepeatFor  2  (Intro)  THEN  (At  \mkleeneopen{}\mBbbU{}\{i''\}\mkleeneclose{}  Intro\mcdot{}  THEN  Try  (Complete  ((MemCD  THEN  Auto))))  THEN  Intros)
  THEN  Unfold  `per-eq-def`  0\mcdot{}
  THEN  Auto)

---

Home Index