Prove.thy
2009-10-24 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall)
less more (0) -1 tip