|intros;unfold;intro;inversion H5
[intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4;
rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4)
|intros;lapply (inj_tail ? ? ? ? ? H9);
rewrite < Hletin1 in H6;lapply (H1 a1)
[apply (Hletin2 H6)
|intros;unfold;intro;inversion H5
[intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4;
rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4)
|intros;lapply (inj_tail ? ? ? ? ? H9);
rewrite < Hletin1 in H6;lapply (H1 a1)
[apply (Hletin2 H6)