## Stream: general

### Topic: injections

#### Johan Commelin (Sep 17 2019 at 07:52):

I learnt from #1453 about the existence of an injections tactic. What does it do? Should it be documented?

#### Mario Carneiro (Sep 17 2019 at 07:53):

it's basically repeat {injection}, casing on everything in the context

#### Johan Commelin (Sep 17 2019 at 07:55):

Aha, what does injection do? Should it be documented?

#### Chris Hughes (Sep 17 2019 at 08:01):

It basically just proves that constructors to inductive types are injective. So I can use it to prove x = y and l1 = l2 from x::l1 = y::l2