proposition: Theorem stripInRzIn1 : forall (L : list rNat) (L1 : list rZ) (a : rZ), In a (stripInRz L L1) -> In (valRz a) L.
proof: Proof. intros L L1; elim L1; simpl in |- *; auto with stalmarck. intros a H'; elim H'; auto with stalmarck. intros a l H' a0. case (In_dec rNatDec (valRz a) L); simpl in |- *; auto with stalmarck. intros H'0 H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ]; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)