[PPL-devel] Proof