---

Step * 1 of Lemma mrec-induction2


1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
⊢ ∀x:mobj(L). P[x]
BY
{ ((InstLemma `mrec-induction` [⌜L⌝;⌜P⌝]⋅ THENW Auto) THENM Trivial) }

1
.....antecedent..... 
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
⊢ ∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . P[z]) ⇒ P[x])

---

Latex:

---

Latex:

1.  L  :  MutualRectypeSpec
2.  [P]  :  mobj(L)  {}\mrightarrow{}  TYPE
3.  mrecind(L;x.P[x])
\mvdash{}  \mforall{}x:mobj(L).  P[x]


By

---

Latex:
((InstLemma  `mrec-induction`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENW  Auto)  THENM  Trivial)

---

Home Index