PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: closed tapp

t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2)
By:
Unfold `closed_term` 0
THEN
Unfold `term_free_vars` 0
THEN
Reduce 0
THEN
Fold `term_free_vars` 0
THEN
RWW "append_is_nil" 0
Generated subgoals:

None

About:
andall

PrintForm Definitions mb automata 2 Sections GenAutomata Doc