fact: Definition valid_triple (ps : (states * states) * states) := ((forall s, In s (fst (fst ps)) -> valid_state s) /\ (forall s, In s (snd (fst ps)) -> valid_state s)) /\ (forall s, In s (snd ps) -> valid_state s).
imports: ZArith List