/3 width=4 by inj, ex3_intro/
| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
#L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
/3 width=4 by inj, ex3_intro/
| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
#L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K