HomeIsabelle/Phabricator

replaced some lemmas' implicit formulas by explicit ones to avoid silent changes