#h #g #L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
elim (cnr_dec L T1) /3 width=3/
* #T #H1T1 #H2T1
elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/
qed.
#h #g #L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
elim (cnr_dec L T1) /3 width=3/
* #T #H1T1 #H2T1
elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/
qed.