Post #1846836

@jonmsterling Or did you mean congruence of definitional equality and specifically the xi rule / conversion under lambda? Pédrot's paper achieves it, unlike previous attempts. @mevenlennonbertrand @jpoiret @carloangiuli