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