Post #1846838

@jonmsterling @jeanas @jpoiret @carloangiuli The core idea is perhaps unsurprising: if you only quote close normal forms, everything is fine wrt to congruence. Still, this gives a very direct construction for "relevant" CT (the one with a Sigma type).