- [apply ex_intro
- [apply O
- |intros;unfold;intro;inversion H1
- [intros;lapply (sym_eq ? ? ? H3);absurd (a::l1 = [])
- [assumption|apply nil_cons]
- |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = [])
- [assumption|apply nil_cons]]]
- |elim H;lapply (decidable_eq_nat a t);elim Hletin
- [apply ex_intro
- [apply (S a)
- |intros;unfold;intro;inversion H4
- [intros;lapply (inj_head_nat ? ? ? ? H6);rewrite < Hletin1 in H5;
- rewrite < H2 in H5;rewrite > H5 in H3;
- apply (not_le_Sn_n ? H3)
- |intros;lapply (inj_tail ? ? ? ? ? H8);rewrite < Hletin1 in H5;
- rewrite < H7 in H5;
- apply (H1 m ? H5);lapply (le_S ? ? H3);
- apply (le_S_S_to_le ? ? Hletin2)]]
- |cut ((leb a t) = true \lor (leb a t) = false)
- [elim Hcut
- [apply ex_intro
- [apply (S t)
- |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)
- |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2;
- simplify in Hletin2;rewrite < H8;
- apply (trans_le ? ? ? Hletin2);
- apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]]
- |apply ex_intro
- [apply a
- |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1;
- simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1);
- unfold in Hletin2;unfold;intro;inversion H5
- [intros;lapply (inj_head_nat ? ? ? ? H7);
- rewrite < Hletin3 in H6;rewrite > H6 in H4;
- apply (Hletin1 H4)
- |intros;lapply (inj_tail ? ? ? ? ? H9);
- rewrite < Hletin3 in H6;rewrite < H8 in H6;
- apply (H1 ? H4 H6)]]]
- |elim (leb a t);autobatch]]]]
+ [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1)
+ |elim H;
+ apply (ex_intro ? ? (S (max a t))).
+ intros.unfold. intro.
+ elim (in_cons_case ? ? ? ? H3)
+ [rewrite > H4 in H2.autobatch
+ |elim H4.apply (H1 m ? H6).
+ apply (trans_le ? (max a t));autobatch]]]