proposition: Remark P_F_Infinite : forall l:LList A, P l -> satisfies l (F_Infinite (Atomic (eq a))).
proof: Proof. unfold F_Infinite in |- *. cofix P_F_Infinite. intro l; simple destruct 1. - intro eg; rewrite eg; unfold w_omega in |- *; rewrite omega_of_Finite. + unfold w in |- *; autorewrite with llists using auto with llists. split. auto with llists. apply P_F_Infinite. unfold P in |- *; auto. + unfold w in |- *; auto with llists. - intro eg; rewrite eg. unfold w_omega in |- *; rewrite omega_of_Finite. + unfold w in |- *; rewrite LAppend_LCons; split. auto with llists. apply P_F_Infinite. unfold P in |- *; left. rewrite <- LAppend_LCons, <- omega_of_Finite; auto with llists. + unfold w;auto with llists. Qed.
imports: Arith List RelationClasses