---

Step * of Lemma prior-as-rec-bind-class_wf

∀[Info,A:Type]. ∀[X:EClass(A)].  (prior-as-rec-bind-class(X) ∈ EClass(A))
BY
{ (ProveWfLemma
   THEN Assert ⌜rec-bind-class(λi.prior-as-rec-bind-class-out(i);λi.prior-as-rec-bind-class-in(X;i))
                ∈ (bag(A) + (bag(A)?)) ⟶ EClass(A)⌝⋅
   THEN Auto
   THEN Reduce 0
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN ((InstLemma `prior-as-rec-bind-class-in-property` [⌜Info⌝;⌜A⌝;⌜X⌝;⌜x⌝]⋅ THENM BHyp -1 ) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].    (prior-as-rec-bind-class(X)  \mmember{}  EClass(A))


By

---

Latex:
(ProveWfLemma
  THEN  Assert  \mkleeneopen{}rec-bind-class(\mlambda{}i.prior-as-rec-bind-class-out(i);\mlambda{}i.prior-as-rec-bind-class-in(X;i))
                            \mmember{}  (bag(A)  +  (bag(A)?))  {}\mrightarrow{}  EClass(A)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  ((InstLemma  `prior-as-rec-bind-class-in-property`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  BHyp  -1  )
              THEN  Auto
              )\mcdot{})

---

Home Index