fact: Definition restrictState (S : State) (L : list rNat) : State := match eqStateRzContrDec S with | left _ => (rZTrue, rZFalse) :: nil | right _ => stripRzDec S (prodRz (stripInRz L (stripRz S)) (stripInRz L (stripRz S))) end.
imports: Stalmarck(stalmarck) Stalmarck(ltState)