Jonas Kaiser, Tobias Tebbi, Gert Smolka: Equivalence of system f and ź2 in Coq based on context morphism lemmas. CPP 2017: 222-234