proposition: Lemma ok_LNil {A: Type}: forall X:LList A -> Prop, Infinite_ok X -> ~ X LNil.
proof: Proof. unfold Infinite_ok. intros X H H0; case (H LNil). - assumption. - intros x H1; case H1; intros x0 H2; case H2; discriminate 1. Qed.