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