---

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

∀[Info,A:Type]. ∀[X:EClass(A)].  (prior-as-rec-bind-class2(X) ∈ EClass(A))
BY
{ (ProveWfLemma
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN ((InstLemma `prior-as-rec-bind-class-in2-property` [⌜Info⌝;⌜A⌝;⌜X⌝;⌜x⌝]⋅ THENM BHyp -1 ) THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  ((InstLemma  `prior-as-rec-bind-class-in2-property`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  BHyp  -1  )
              THEN  Auto
              )\mcdot{})

---

Home Index