#C #A #i #f #B #R #Hf #c #b1 #b2 #H elim H -b2 /2 width=1 by ltc_rc/
#b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/
qed.
#C #A #i #f #B #R #Hf #c #b1 #b2 #H elim H -b2 /2 width=1 by ltc_rc/
#b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/
qed.