-| move_wolf: ∀g,w,w1,c. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 w w1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c w) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w1 c w1)
-| move_cabbage: ∀g,w,c,c1.\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 c c1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c c) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c1 c1)
-| move_boat: ∀g,w,c,b,b1. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 b b1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c b) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c b1).
+| move_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1)
+| move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1)
+| move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1).