fact: Fixpoint stripInRz (L : list rNat) (L1 : list rZ) {struct L1} : list rZ := match L1 with | nil => nil | a :: L1' => match In_dec rNatDec (valRz a) L with | left _ => a :: stripInRz L L1' | right _ => stripInRz L L1' end end.
imports: Stalmarck(stalmarck) Stalmarck(ltState)