Structural induction on lazy lists

For an admissible predicate on lazy lists $P$, prove $P(\perp )$ and $P([])$, and prove $P(xs)\Rightarrow P(x:xs)$ for every possibly partial head $x$. Constructor induction then establishes $P$ on every finite partial approximation, and admissibility extends it to limits, including infinite lists. Without the bottom value case and the limit condition, ordinary finite structural induction does not justify a claim about infinite data.^[ref]