-(∀w.(\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2))→ \ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2〉)
- →∀w.\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2〉.
+(∀w.(\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2))→ \ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2〉)
+ →∀w.\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2〉.