---

Step * of Lemma language1_wf

∀[fml:D:Type ⟶ ℙ ⟶ (D ⟶ ℙ) ⟶ (D ⟶ ℙ) ⟶ (D ⟶ D ⟶ ℙ) ⟶ (D ⟶ D ⟶ ℙ) ⟶ (D ⟶ D ⟶ ℙ) ⟶ (D ⟶ D ⟶ D ⟶ ℙ) ⟶ ℙ]
  (language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ∈ ℙ')
BY
{ (ProveWfLemma THEN Try (Unfold `so_apply` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[fml:D:Type
            {}\mrightarrow{}  \mBbbP{}
            {}\mrightarrow{}  (D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  \mBbbP{}]
    (language1\{i:l\}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H])  \mmember{}  \mBbbP{}')


By

---

Latex:
(ProveWfLemma  THEN  Try  (Unfold  `so\_apply`  0)  THEN  Auto)

---

Home Index