Tuned some Latex text
Some cosmetic changes
Minor cosmetic changes
Tuned text
Tuned text
wip
Added proof for size bounds of certificates
Polished proof for lemma size_pratt_fpc
reformatting
tune whitespace
AFP cleanups