proposition: Lemma ok_LCons {A: Type} : forall (X:LList A -> Prop) (a:A) (l:LList A), Infinite_ok X -> X (LCons a l) -> X l.
proof: Proof. intros X a l H H0; case (H (LCons a l)). - assumption. - simple destruct 1; intros x0 H2; case H2; injection 1. simple destruct 1; auto. Qed.