Talk:Proof compression