theorem ljoineq (_L1 _L2: nat): $ _L1 = _L2 -> ljoin _L1 = ljoin _L2 $;
_L1 = _L2 -> _L1 = _L2
_L1 = _L2 -> ljoin _L1 = ljoin _L2