Add defs about linear universal quantifications.
Add autoapply instance about LWith.
Add defs about linear existential quantifications.