+
+lemma TokP : ∀t,C.reflect (Tok t C) (Tok_dec C t).
+intros; apply prove_reflect; generalize in match C; elim t; intros;
+[1,2,3,4,5,6,7: apply rule #; simplify in H H1 H2;
+ [1: apply (b2pT ?? (cmpCP ??) H);
+ |2,7: cases (b2pT ?? (andbP ??) H1); apply (b2pT ?? (lebP ??)); assumption;
+ |3,6: cases (b2pT ?? (andbP ??) H1); autobatch depth=2;
+ |4,5,9,10,13: cases (b2pT ?? (andbP ??) H2); autobatch depth=2;
+ |8: autobatch depth=2;
+ |11: cases (b2pT ?? (andbP ??) H2); cases (b2pT ?? (andbP ??) H4);
+ apply (b2pT ?? (lebP ??)); assumption;
+ |12,11: cases (b2pT ?? (andbP ??) H2); cases (b2pT ?? (andbP ??) H4); autobatch depth=2;]
+|*: intro E; inversion E; clear E; intros; simplify in H;
+ [1: destruct H3; destruct H2; rewrite > H1 in H; normalize in H; destruct H;
+ |9: destruct H6; destruct H5; simplify in H1;
+ cases (b2pF ?? (andbP ??) H1); split[2:apply (p2bT ?? (lebP ??) H4);]
+ lapply depth=0 (H (Reg::l)) as W; cases (Tok_dec (Reg::l) p) in W;
+ intros; [reflexivity] cases (H5 ? H2); reflexivity;
+ |17: destruct H7; destruct H8; simplify in H2; apply (b2pF ?? (andbP ??) H2);
+ lapply depth=0 (H l) as W1; lapply depth=0 (H1 l) as W2;
+ cases (Tok_dec l p) in W1; cases (Tok_dec l p1) in W2;
+ intros; split; try reflexivity;
+ [1,3: cases (H7 ? H5); reflexivity;|*: cases (H8 ? H3); reflexivity;]
+ |25: destruct H6; destruct H5; simplify in H1;
+ apply (b2pF ?? (andbP ??) H1); rewrite > (p2bT ?? (lebP ??) H2);
+ split[reflexivity] lapply depth=0 (H (mapb l)) as W;
+ cases (Tok_dec (mapb l) p) in W; intros; [reflexivity]
+ cases (H5 ? H3); reflexivity;
+ |33: destruct H5; destruct H4; simplify in H1; exact (H ? H1 H2);
+ |41: destruct H8; destruct H6; destruct H7; clear H4 H6; simplify in H2;
+ lapply depth=0 (H l) as W1; lapply depth=0 (H1 (Ban::l)) as W2;
+ apply (b2pF ?? (andbP ??) H2); cases (Tok_dec l p) in W1;
+ cases (Tok_dec (Ban::l) p1) in W2; intros; split; try reflexivity;
+ [1,3: cases (H4 ? H5); reflexivity;|*: cases (H6 ? H3); reflexivity;]
+ |49: destruct H9; destruct H8; clear H6 H4; simplify in H2;
+ apply (b2pF ?? (andbP ??) H2); clear H2; rewrite > (p2bT ?? (lebP ??) H7);
+ rewrite > andb_sym; simplify;
+ lapply depth=0 (H l) as W1; lapply depth=0 (H1 (Sec::l)) as W2;
+ cases (Tok_dec l p) in W1; cases (Tok_dec (Sec::l) p1) in W2;
+ intros; split; try reflexivity;
+ [1,3: cases (H2 ? H5); reflexivity;|*: cases (H4 ? H3); reflexivity;]
+ |*: try solve[destruct H3]; try solve[destruct H4]; try solve[destruct H5];
+ try solve[destruct H6]; try solve[destruct H7]; try solve[destruct H8]]]