add properties of provability required for truth lemma in fol/seq/prv