Step
*
of Lemma
pv11_p1_add_if_new_wf
pv11_p1_add_if_new() ∈ ∩A:𝕌'. ((A ─→ A ─→ 𝔹) ─→ A ─→ (A List) ─→ (A List))
BY
{ ProveEmlWfLemma }
Latex:
Latex:
pv11\_p1\_add\_if\_new()  \mmember{}  \mcap{}A:\mBbbU{}'.  ((A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  A  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  (A  List))
By
Latex:
ProveEmlWfLemma
Home
Index