elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * /2 width=1 by conj/
#HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/
qed-.
elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * /2 width=1 by conj/
#HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/
qed-.