fact: Definition nexts_correct (ps : states * states) s : (forall s1, In s1 (fst (nexts ps s)) <-> In s1 (fst ps) \/ exists f, In f movel /\ s1 = f s /\ ~ In s1 (fst ps)) /\ (forall s1, In s1 (snd (nexts ps s)) <-> In s1 (snd ps) \/ exists f, In f movel /\ s1 = f s /\ ~ In s1 (fst ps)).
imports: ZArith List