---

Step * of Lemma provisional-apply2_wf

No Annotations
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[a:Provisional(A)]. ∀[b:Provisional(B)].  (provisional-apply2(f;a;b) ∈ Provisional(C))
BY
{ (ProveWfLemma THEN D -1 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[a:Provisional(A)].  \mforall{}[b:Provisional(B)].
    (provisional-apply2(f;a;b)  \mmember{}  Provisional(C))


By

---

Latex:
(ProveWfLemma  THEN  D  -1  THEN  Unhide  THEN  Auto)

---

Home Index