proposition: Theorem F_Infinite_cons (P:LList A -> Prop) : forall (a:A) (l:LList A), satisfies l (F_Infinite P) -> satisfies (LCons a l) (F_Infinite P).
proof: Proof. split. - inversion H; now right. - assumption. Qed.
imports: Arith List RelationClasses