---

Step * of Lemma mkGame_wf

∀[L,R:Type]. ∀[f:L ⟶ Game]. ∀[g:R ⟶ Game].  ({mkGame(f[a] with a:L | g[b] with b:R} ∈ Game)
BY
{ ((InstLemma `Wsup_wf` [⌜parm{i'}⌝;⌜GameA{i:l}()⌝;⌜λ2LR.GameB(LR)⌝]⋅ THENA Auto)
   THEN Fold `Game` (-1)
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[L,R:Type].  \mforall{}[f:L  {}\mrightarrow{}  Game].  \mforall{}[g:R  {}\mrightarrow{}  Game].    (\{mkGame(f[a]  with  a:L  |  g[b]  with  b:R\}  \mmember{}  Game)


By

---

Latex:
((InstLemma  `Wsup\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}GameA\{i:l\}()\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}LR.GameB(LR)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `Game`  (-1)
  THEN  ProveWfLemma)

---

Home Index