[ apply (mk_finType fsort enum Hcut)
| intros (x); cases x (n Hn); simplify in Hn; clear x;
generalize in match Hn; generalize in match Hn; clear Hn;
[ apply (mk_finType fsort enum Hcut)
| intros (x); cases x (n Hn); simplify in Hn; clear x;
generalize in match Hn; generalize in match Hn; clear Hn;
unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
[2:rewrite > IH; [1,3: autobatch]
unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
[2:rewrite > IH; [1,3: autobatch]
fold simplify (sort nat_eqType); (* CANONICAL?! *)
cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
simplify; [2: reflexivity]
fold simplify (sort nat_eqType); (* CANONICAL?! *)
cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
simplify; [2: reflexivity]
- generalize in match H1; clear H1; cases s; clear s; intros (H1);
- unfold segment; simplify; simplify in H1; rewrite > H1;
+ generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1);
+ unfold fsort; unfold segment; simplify; simplify in H1; rewrite > H1;
rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
unfold Not; intros (Enw); rewrite > Enw in Hw;
rewrite > ltb_refl in Hw; destruct Hw]
rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
unfold Not; intros (Enw); rewrite > Enw in Hw;
rewrite > ltb_refl in Hw; destruct Hw]
lemma uniqP : ∀d:eqType.∀l:list d.
reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
lemma uniqP : ∀d:eqType.∀l:list d.
reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
unfold Not; intros (A); lapply (A t) as A';
[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
destruct A'; rewrite < count_O_mem in H1;
unfold Not; intros (A); lapply (A t) as A';
[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
destruct A'; rewrite < count_O_mem in H1;
|2: simplify; rewrite > cmp_refl; reflexivity;]
|2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
intros (r Mrl1); lapply (A r);
|2: simplify; rewrite > cmp_refl; reflexivity;]
|2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
intros (r Mrl1); lapply (A r);
generalize in match Hletin1; simplify; apply (cmpP d r t);
simplify; intros (E Hc); [2: assumption]
destruct Hc; rewrite < count_O_mem in Mrl1;
generalize in match Hletin1; simplify; apply (cmpP d r t);
simplify; intros (E Hc); [2: assumption]
destruct Hc; rewrite < count_O_mem in Mrl1;
intros (d p x); cases x (t Ht); clear x;
generalize in match (mem_finType d t);
generalize in match (uniq_fintype_enum d);
intros (d p x); cases x (t Ht); clear x;
generalize in match (mem_finType d t);
generalize in match (uniq_fintype_enum d);
cases (in_sub_eq d p t1); simplify;
[1:generalize in match H3; clear H3; cases s (r Hr); clear s;
simplify; intros (Ert1); generalize in match Hr; clear Hr;
cases (in_sub_eq d p t1); simplify;
[1:generalize in match H3; clear H3; cases s (r Hr); clear s;
simplify; intros (Ert1); generalize in match Hr; clear Hr;