[WIP] External lemma to deal with the conversion needed in EqSubstJ
[WIP] External lemma to deal with the conversion needed in EqSubstJ

This should make things clearer. I hope this will also be smaller. In
any case it is a very long proof and it sounds better to have it as a
lemma since it will be used twice.

TheoWinterhalter/formal-type-theory