Adapt pf_induct to require permutation property.