package proofs