---

Step * of Lemma es-propagation-rule-iff_wf

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[f:Id ⟶ A ⟶ B]. ∀[g:A ⟶ (Id List)]. ∀[es:EO+(Info)].
  (X ⇐f⇒ Y@g ∈ ℙ)
BY
{ ProveWfLemma⋅ }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[g:A  {}\mrightarrow{}  (Id  List)].
\mforall{}[es:EO+(Info)].
    (X  \mLeftarrow{}{}f{}\mRightarrow{}  Y@g  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma\mcdot{}

---

Home Index