Level: Lib Thy Top: 1
Hypotheses:

  1. e :

  2. L : List

  3. M : List

Conclusion:

||e:L @ M|| = ||e:L|| + ||e:M||

Applied Tactic: ListInd 2
Generated subgoals:

1. ||e:[] @ M|| = ||e:[]|| + ||e:M||

2. ||e:(u::v) @ M|| = ||e:u::v|| + ||e:M||