---

Step * of Lemma mFOLRule_ind_wf_simple

∀[A:Type]. ∀[v:mFOLRule()]. ∀[andI,impI:A]. ∀[allI,existsI:var:ℤ ─→ A]. ∀[orI:left:𝔹 ─→ A]. ∀[hyp:A].
∀[andE,orE,impE:hypnum:ℕ ─→ A]. ∀[allE,existsE:hypnum:ℕ ─→ var:ℤ ─→ A].
  (mFOLRule_ind(v;
   andI;
   impI;
   var.allI[var];
   var.existsI[var];
   left.orI[left];
   hyp;hypnum.andE[hypnum];
   hypnum.orE[hypnum];
   hypnum.impE[hypnum];
   hypnum,var.allE[hypnum;var];
   hypnum,var.existsE[hypnum;var]) ∈ A)
BY
{ ProveDatatypeIndWfSimple 0 `mFOLRule_ind_wf` }

---

Latex:


\mforall{}[A:Type].  \mforall{}[v:mFOLRule()].  \mforall{}[andI,impI:A].  \mforall{}[allI,existsI:var:\mBbbZ{}  {}\mrightarrow{}  A].  \mforall{}[orI:left:\mBbbB{}  {}\mrightarrow{}  A].
\mforall{}[hyp:A].  \mforall{}[andE,orE,impE:hypnum:\mBbbN{}  {}\mrightarrow{}  A].  \mforall{}[allE,existsE:hypnum:\mBbbN{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  A].
    (mFOLRule\_ind(v;
      andI;
      impI;
      var.allI[var];
      var.existsI[var];
      left.orI[left];
      hyp;hypnum.andE[hypnum];
      hypnum.orE[hypnum];
      hypnum.impE[hypnum];
      hypnum,var.allE[hypnum;var];
      hypnum,var.existsE[hypnum;var])  \mmember{}  A)


By

ProveDatatypeIndWfSimple  0  `mFOLRule\_ind\_wf`

---

Home Index