add leq-Fin and many of the easy parts of the lemma proofs