Step
*
1
of Lemma
is_list_axiom_lemma
is-list(Ax) ~ tt
BY
{ Try (RW (AddrC [1] (RecUnfoldTopC `is-list` ANDTHENC (TagC (mk_tag_term 3)))) 0)⋅ }
1
tt ~ tt
Latex:
Latex:
is-list(Ax)  \msim{}  tt
By
Latex:
Try  (RW  (AddrC  [1]  (RecUnfoldTopC  `is-list`  ANDTHENC  (TagC  (mk\_tag\_term  3))))  0)\mcdot{}
Home
Index