(**************************************************************************)
include "ground_2/lib/ltc.ma".
(**************************************************************************)
include "ground_2/lib/ltc.ma".
| #n1 #n2 #K #K2 #_ #IH #HK2 #f2 #Hf
elim (IH … Hf) -K1 -IH #L #H1L1 #HLK #H2L1
elim (HR … HLK … HK2 … Hf) -f1 -K -HR
| #n1 #n2 #K #K2 #_ #IH #HK2 #f2 #Hf
elim (IH … Hf) -K1 -IH #L #H1L1 #HLK #H2L1
elim (HR … HLK … HK2 … Hf) -f1 -K -HR