[cases (\ 5a href="cic:/matita/tutorial/chapter10/memb_sons.def(8)"\ 6memb_sons\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6memb_filter_memb\ 5/a\ 6 … H)) -H
#a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (w1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])))
>\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >mw1 >mw2 >m1 >m2 % //
|@r_frontier @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
]
[cases (\ 5a href="cic:/matita/tutorial/chapter10/memb_sons.def(8)"\ 6memb_sons\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6memb_filter_memb\ 5/a\ 6 … H)) -H
#a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (w1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])))
>\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >mw1 >mw2 >m1 >m2 % //
|@r_frontier @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
]