Added sizes to bisimilarity
Began proof that extensional equality implies bisimilarity