-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcoqindex.html
8845 lines (8838 loc) · 772 KB
/
coqindex.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Index</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<div id="page">
<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: Logical Foundations</a></div>
<ul id='menu'>
<li class='section_name'><a href='toc.html'>Table of Contents</a></li>
<li class='section_name'><a href='coqindex.html'>Index</a></li>
<li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>
<div id="main">
<table>
<tr>
<td>Global Index</td>
<td><a href="coqindex.html#global_A">A</a></td>
<td><a href="coqindex.html#global_B">B</a></td>
<td><a href="coqindex.html#global_C">C</a></td>
<td><a href="coqindex.html#global_D">D</a></td>
<td><a href="coqindex.html#global_E">E</a></td>
<td><a href="coqindex.html#global_F">F</a></td>
<td><a href="coqindex.html#global_G">G</a></td>
<td><a href="coqindex.html#global_H">H</a></td>
<td><a href="coqindex.html#global_I">I</a></td>
<td><a href="coqindex.html#global_J">J</a></td>
<td><a href="coqindex.html#global_K">K</a></td>
<td><a href="coqindex.html#global_L">L</a></td>
<td><a href="coqindex.html#global_M">M</a></td>
<td><a href="coqindex.html#global_N">N</a></td>
<td><a href="coqindex.html#global_O">O</a></td>
<td><a href="coqindex.html#global_P">P</a></td>
<td><a href="coqindex.html#global_Q">Q</a></td>
<td><a href="coqindex.html#global_R">R</a></td>
<td><a href="coqindex.html#global_S">S</a></td>
<td><a href="coqindex.html#global_T">T</a></td>
<td><a href="coqindex.html#global_U">U</a></td>
<td><a href="coqindex.html#global_V">V</a></td>
<td><a href="coqindex.html#global_W">W</a></td>
<td><a href="coqindex.html#global_X">X</a></td>
<td><a href="coqindex.html#global_Y">Y</a></td>
<td><a href="coqindex.html#global_Z">Z</a></td>
<td>_</td>
<td><a href="coqindex.html#global_*">other</a></td>
<td>(3992 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
<td><a href="coqindex.html#notation_A">A</a></td>
<td><a href="coqindex.html#notation_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#notation_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#notation_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#notation_L">L</a></td>
<td>M</td>
<td><a href="coqindex.html#notation_N">N</a></td>
<td>O</td>
<td><a href="coqindex.html#notation_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#notation_R">R</a></td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td><a href="coqindex.html#notation_*">other</a></td>
<td>(86 entries)</td>
</tr>
<tr>
<td>Binder Index</td>
<td><a href="coqindex.html#binder_A">A</a></td>
<td><a href="coqindex.html#binder_B">B</a></td>
<td><a href="coqindex.html#binder_C">C</a></td>
<td><a href="coqindex.html#binder_D">D</a></td>
<td><a href="coqindex.html#binder_E">E</a></td>
<td><a href="coqindex.html#binder_F">F</a></td>
<td><a href="coqindex.html#binder_G">G</a></td>
<td><a href="coqindex.html#binder_H">H</a></td>
<td><a href="coqindex.html#binder_I">I</a></td>
<td><a href="coqindex.html#binder_J">J</a></td>
<td><a href="coqindex.html#binder_K">K</a></td>
<td><a href="coqindex.html#binder_L">L</a></td>
<td><a href="coqindex.html#binder_M">M</a></td>
<td><a href="coqindex.html#binder_N">N</a></td>
<td><a href="coqindex.html#binder_O">O</a></td>
<td><a href="coqindex.html#binder_P">P</a></td>
<td><a href="coqindex.html#binder_Q">Q</a></td>
<td><a href="coqindex.html#binder_R">R</a></td>
<td><a href="coqindex.html#binder_S">S</a></td>
<td><a href="coqindex.html#binder_T">T</a></td>
<td><a href="coqindex.html#binder_U">U</a></td>
<td><a href="coqindex.html#binder_V">V</a></td>
<td><a href="coqindex.html#binder_W">W</a></td>
<td><a href="coqindex.html#binder_X">X</a></td>
<td><a href="coqindex.html#binder_Y">Y</a></td>
<td><a href="coqindex.html#binder_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(2406 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="coqindex.html#module_A">A</a></td>
<td><a href="coqindex.html#module_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#module_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#module_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#module_L">L</a></td>
<td><a href="coqindex.html#module_M">M</a></td>
<td><a href="coqindex.html#module_N">N</a></td>
<td><a href="coqindex.html#module_O">O</a></td>
<td><a href="coqindex.html#module_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#module_R">R</a></td>
<td>S</td>
<td><a href="coqindex.html#module_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(33 entries)</td>
</tr>
<tr>
<td>Library Index</td>
<td><a href="coqindex.html#library_A">A</a></td>
<td><a href="coqindex.html#library_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#library_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#library_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#library_L">L</a></td>
<td><a href="coqindex.html#library_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#library_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#library_R">R</a></td>
<td>S</td>
<td><a href="coqindex.html#library_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(20 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
<td><a href="coqindex.html#lemma_A">A</a></td>
<td><a href="coqindex.html#lemma_B">B</a></td>
<td><a href="coqindex.html#lemma_C">C</a></td>
<td><a href="coqindex.html#lemma_D">D</a></td>
<td><a href="coqindex.html#lemma_E">E</a></td>
<td><a href="coqindex.html#lemma_F">F</a></td>
<td>G</td>
<td><a href="coqindex.html#lemma_H">H</a></td>
<td><a href="coqindex.html#lemma_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#lemma_L">L</a></td>
<td><a href="coqindex.html#lemma_M">M</a></td>
<td><a href="coqindex.html#lemma_N">N</a></td>
<td><a href="coqindex.html#lemma_O">O</a></td>
<td><a href="coqindex.html#lemma_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#lemma_R">R</a></td>
<td><a href="coqindex.html#lemma_S">S</a></td>
<td><a href="coqindex.html#lemma_T">T</a></td>
<td><a href="coqindex.html#lemma_U">U</a></td>
<td>V</td>
<td><a href="coqindex.html#lemma_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="coqindex.html#lemma_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(498 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
<td><a href="coqindex.html#constructor_A">A</a></td>
<td><a href="coqindex.html#constructor_B">B</a></td>
<td><a href="coqindex.html#constructor_C">C</a></td>
<td><a href="coqindex.html#constructor_D">D</a></td>
<td><a href="coqindex.html#constructor_E">E</a></td>
<td><a href="coqindex.html#constructor_F">F</a></td>
<td><a href="coqindex.html#constructor_G">G</a></td>
<td>H</td>
<td><a href="coqindex.html#constructor_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#constructor_L">L</a></td>
<td><a href="coqindex.html#constructor_M">M</a></td>
<td><a href="coqindex.html#constructor_N">N</a></td>
<td><a href="coqindex.html#constructor_O">O</a></td>
<td><a href="coqindex.html#constructor_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#constructor_R">R</a></td>
<td><a href="coqindex.html#constructor_S">S</a></td>
<td><a href="coqindex.html#constructor_T">T</a></td>
<td><a href="coqindex.html#constructor_U">U</a></td>
<td>V</td>
<td><a href="coqindex.html#constructor_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="coqindex.html#constructor_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(262 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
<td>A</td>
<td>B</td>
<td><a href="coqindex.html#axiom_C">C</a></td>
<td>D</td>
<td>E</td>
<td><a href="coqindex.html#axiom_F">F</a></td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(2 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
<td><a href="coqindex.html#inductive_A">A</a></td>
<td><a href="coqindex.html#inductive_B">B</a></td>
<td><a href="coqindex.html#inductive_C">C</a></td>
<td><a href="coqindex.html#inductive_D">D</a></td>
<td><a href="coqindex.html#inductive_E">E</a></td>
<td><a href="coqindex.html#inductive_F">F</a></td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#inductive_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#inductive_L">L</a></td>
<td><a href="coqindex.html#inductive_M">M</a></td>
<td><a href="coqindex.html#inductive_N">N</a></td>
<td><a href="coqindex.html#inductive_O">O</a></td>
<td><a href="coqindex.html#inductive_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#inductive_R">R</a></td>
<td><a href="coqindex.html#inductive_S">S</a></td>
<td><a href="coqindex.html#inductive_T">T</a></td>
<td>U</td>
<td>V</td>
<td><a href="coqindex.html#inductive_W">W</a></td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(99 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
<td><a href="coqindex.html#definition_A">A</a></td>
<td><a href="coqindex.html#definition_B">B</a></td>
<td><a href="coqindex.html#definition_C">C</a></td>
<td><a href="coqindex.html#definition_D">D</a></td>
<td><a href="coqindex.html#definition_E">E</a></td>
<td><a href="coqindex.html#definition_F">F</a></td>
<td>G</td>
<td><a href="coqindex.html#definition_H">H</a></td>
<td><a href="coqindex.html#definition_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#definition_L">L</a></td>
<td><a href="coqindex.html#definition_M">M</a></td>
<td><a href="coqindex.html#definition_N">N</a></td>
<td><a href="coqindex.html#definition_O">O</a></td>
<td><a href="coqindex.html#definition_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#definition_R">R</a></td>
<td><a href="coqindex.html#definition_S">S</a></td>
<td><a href="coqindex.html#definition_T">T</a></td>
<td><a href="coqindex.html#definition_U">U</a></td>
<td>V</td>
<td><a href="coqindex.html#definition_W">W</a></td>
<td><a href="coqindex.html#definition_X">X</a></td>
<td><a href="coqindex.html#definition_Y">Y</a></td>
<td><a href="coqindex.html#definition_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(586 entries)</td>
</tr>
</table>
<hr/>
<h1>Global Index</h1>
<a id="global_A"></a><h2>A </h2>
<a href="ImpParser.html#acc:17">acc:17</a> [binder, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="ImpParser.html#acc:36">acc:36</a> [binder, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="Logic.html#add_comm3_take3">add_comm3_take3</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#add_comm3_take2">add_comm3_take2</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#add_comm3">add_comm3</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Induction.html#add_shuffle3'">add_shuffle3'</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_shuffle3">add_shuffle3</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_assoc''">add_assoc''</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_assoc'">add_assoc'</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_assoc">add_assoc</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_comm">add_comm</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_0_r">add_0_r</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_0_r_secondtry">add_0_r_secondtry</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#add_0_r_firsttry">add_0_r_firsttry</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="IndPrinciples.html#add_comm''">add_comm''</a> [lemma, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#add_comm'">add_comm'</a> [lemma, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#add_assoc'">add_assoc'</a> [lemma, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndProp.html#add_le_cases">add_le_cases</a> [lemma, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="AltAuto.html#add_assoc'''">add_assoc'''</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#add_assoc''">add_assoc''</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#add_assoc_from_induction">add_assoc_from_induction</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#add_assoc'">add_assoc'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#add_assoc">add_assoc</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="ProofObjects.html#add1">add1</a> [definition, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="Imp.html#aeval">aeval</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#13e1a0d6f896b2a3e0bf5b7bef0dc598">_ ==> _ (type_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.E_AMult">aevalR_extended.E_AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.E_AMinus">aevalR_extended.E_AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.E_APlus">aevalR_extended.E_APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.E_ANum">aevalR_extended.E_ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.E_Any">aevalR_extended.E_Any</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.aevalR">aevalR_extended.aevalR</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.AMult">aevalR_extended.AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.AMinus">aevalR_extended.AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.APlus">aevalR_extended.APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.ANum">aevalR_extended.ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.AAny">aevalR_extended.AAny</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended.aexp">aevalR_extended.aexp</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_extended">aevalR_extended</a> [module, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#85dec74cb30cb5a47d1089acdd7473e<sub>9</sub>">_ ==> _ (type_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.E_ADiv">aevalR_division.E_ADiv</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.E_AMult">aevalR_division.E_AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.E_AMinus">aevalR_division.E_AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.E_APlus">aevalR_division.E_APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.E_ANum">aevalR_division.E_ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.aevalR">aevalR_division.aevalR</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.ADiv">aevalR_division.ADiv</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.AMult">aevalR_division.AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.AMinus">aevalR_division.AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.APlus">aevalR_division.APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.ANum">aevalR_division.ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division.aexp">aevalR_division.aexp</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aevalR_division">aevalR_division</a> [module, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aexp">aexp</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp">AExp</a> [module, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.add_assoc__lia">AExp.add_assoc__lia</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.add_comm__lia">AExp.add_comm__lia</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aeval">AExp.aeval</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR">AExp.aevalR</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#e388c99d648cf6fa1ed798726c0d097c">_ ==> _ (type_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.HypothesisNames.E_AMult">AExp.aevalR_first_try.HypothesisNames.E_AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.HypothesisNames.E_AMinus">AExp.aevalR_first_try.HypothesisNames.E_AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.HypothesisNames.E_APlus">AExp.aevalR_first_try.HypothesisNames.E_APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.HypothesisNames.E_ANum">AExp.aevalR_first_try.HypothesisNames.E_ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.HypothesisNames.aevalR">AExp.aevalR_first_try.HypothesisNames.aevalR</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.HypothesisNames">AExp.aevalR_first_try.HypothesisNames</a> [module, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.E_AMult">AExp.aevalR_first_try.E_AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.E_AMinus">AExp.aevalR_first_try.E_AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.E_APlus">AExp.aevalR_first_try.E_APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.E_ANum">AExp.aevalR_first_try.E_ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try.aevalR">AExp.aevalR_first_try.aevalR</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aevalR_first_try">AExp.aevalR_first_try</a> [module, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aeval_iff_aevalR'">AExp.aeval_iff_aevalR'</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aeval_iff_aevalR">AExp.aeval_iff_aevalR</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.aexp">AExp.aexp</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.AMinus">AExp.AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.AMult">AExp.AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.ANum">AExp.ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.APlus">AExp.APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BAnd">AExp.BAnd</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BEq">AExp.BEq</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.beval">AExp.beval</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.bevalR">AExp.bevalR</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.beval_iff_bevalR">AExp.beval_iff_bevalR</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.bexp">AExp.bexp</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BFalse">AExp.BFalse</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BGt">AExp.BGt</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BLe">AExp.BLe</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BNeq">AExp.BNeq</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BNot">AExp.BNot</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.BTrue">AExp.BTrue</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.E_AMult">AExp.E_AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.E_AMinus">AExp.E_AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.E_APlus">AExp.E_APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.E_ANum">AExp.E_ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.foo">AExp.foo</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.foo'">AExp.foo'</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.invert_example1">AExp.invert_example1</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.In10">AExp.In10</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.In10'">AExp.In10'</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.manual_grade_for_beval_rules">AExp.manual_grade_for_beval_rules</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.optimize_0plus_b_sound">AExp.optimize_0plus_b_sound</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.optimize_0plus_b">AExp.optimize_0plus_b</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.optimize_0plus_sound''">AExp.optimize_0plus_sound''</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.optimize_0plus_sound'">AExp.optimize_0plus_sound'</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.optimize_0plus_sound">AExp.optimize_0plus_sound</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.optimize_0plus">AExp.optimize_0plus</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.repeat_loop">AExp.repeat_loop</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.silly_presburger_example">AExp.silly_presburger_example</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.silly1">AExp.silly1</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.silly2">AExp.silly2</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.test_optimize_0plus">AExp.test_optimize_0plus</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AExp.test_aeval1">AExp.test_aeval1</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#537bdfcba03c8f3fc0db3931fceaa7d<sub>4</sub>">_ ==>b _ (type_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#16e9a8c0483e29d8b8b35f17eec604fa">_ ==> _ (type_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aexp1">aexp1</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#aexp2">aexp2</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#ae:34">ae:34</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AId">AId</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Logic.html#All">All</a> [definition, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#All_In">All_In</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Induction.html#all3_spec">all3_spec</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="ImpParser.html#alpha">alpha</a> [constructor, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="AltAuto.html">AltAuto</a> [library]<br/>
<a href="Imp.html#AMinus">AMinus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#AMult">AMult</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndProp.html#ancestor_of<sub>1</sub>">ancestor_of<sub>1</sub></a> [definition, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#ancestor_of">ancestor_of</a> [definition, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Basics.html#andb">andb</a> [definition, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb_eq_orb">andb_eq_orb</a> [lemma, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb_commutative''">andb_commutative''</a> [lemma, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb_true_elim2">andb_true_elim2</a> [lemma, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb_commutative'">andb_commutative'</a> [lemma, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb_commutative">andb_commutative</a> [lemma, in <a href="Basics.html">Basics</a>]<br/>
<a href="Logic.html#andb_true_iff">andb_true_iff</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Induction.html#andb_false_r">andb_false_r</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="AltAuto.html#andb_true_elim2'">andb_true_elim2'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#andb_true_elim2">andb_true_elim2</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#andb_commutative'">andb_commutative'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#andb_commutative">andb_commutative</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#andb_eq_orb">andb_eq_orb</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Basics.html#andb'">andb'</a> [definition, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb3">andb3</a> [definition, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#andb3_exchange">andb3_exchange</a> [lemma, in <a href="Basics.html">Basics</a>]<br/>
<a href="AltAuto.html#andb3_exchange'">andb3_exchange'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#andb3_exchange">andb3_exchange</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="ProofObjects.html#and_assoc">and_assoc</a> [definition, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="Logic.html#and_assoc">and_assoc</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_commut">and_commut</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_example3">and_example3</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_example2''">and_example2''</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_example2'">and_example2'</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_example2">and_example2</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_exercise">and_exercise</a> [definition, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_example'">and_example'</a> [definition, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#and_example">and_example</a> [definition, in <a href="Logic.html">Logic</a>]<br/>
<a href="Rel.html#antisymmetric">antisymmetric</a> [definition, in <a href="Rel.html">Rel</a>]<br/>
<a href="Imp.html#ANum">ANum</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#APlus">APlus</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Poly.html#app">app</a> [definition, in <a href="Poly.html">Poly</a>]<br/>
<a href="IndProp.html#App">App</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Logic.html#apply_iff_example2">apply_iff_example2</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#apply_iff_example1">apply_iff_example1</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Maps.html#apply_empty">apply_empty</a> [lemma, in <a href="Maps.html">Maps</a>]<br/>
<a href="Poly.html#app_length">app_length</a> [lemma, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#app_assoc">app_assoc</a> [lemma, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#app_nil_r">app_nil_r</a> [lemma, in <a href="Poly.html">Poly</a>]<br/>
<a href="IndProp.html#app_ne">app_ne</a> [lemma, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#app_exists">app_exists</a> [lemma, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="AltAuto.html#app_nil_r''">app_nil_r''</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#app_nil_r'">app_nil_r'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#app_nil_r">app_nil_r</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#app_length'">app_length'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#app_length">app_length</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Auto.html">Auto</a> [library]<br/>
<a href="Auto.html#auto_example_7'">auto_example_7'</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_7">auto_example_7</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_6'">auto_example_6'</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_6">auto_example_6</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_5'">auto_example_5'</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_5">auto_example_5</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_4">auto_example_4</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_3">auto_example_3</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_2">auto_example_2</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_1'">auto_example_1'</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#auto_example_1">auto_example_1</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="AltAuto.html#auto_example_8">auto_example_8</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_7'">auto_example_7'</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_7">auto_example_7</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_6'">auto_example_6'</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_6">auto_example_6</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_5">auto_example_5</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_4">auto_example_4</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_3">auto_example_3</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_2">auto_example_2</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_1'">auto_example_1'</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#auto_example_1">auto_example_1</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:118">a<sub>1</sub>:118</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:12">a<sub>1</sub>:12</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:120">a<sub>1</sub>:120</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:122">a<sub>1</sub>:122</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:124">a<sub>1</sub>:124</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:129">a<sub>1</sub>:129</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:133">a<sub>1</sub>:133</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:137">a<sub>1</sub>:137</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:14">a<sub>1</sub>:14</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:141">a<sub>1</sub>:141</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:149">a<sub>1</sub>:149</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:151">a<sub>1</sub>:151</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:153">a<sub>1</sub>:153</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:159">a<sub>1</sub>:159</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:16">a<sub>1</sub>:16</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:163">a<sub>1</sub>:163</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:167">a<sub>1</sub>:167</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:175">a<sub>1</sub>:175</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:177">a<sub>1</sub>:177</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:179">a<sub>1</sub>:179</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:18">a<sub>1</sub>:18</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:183">a<sub>1</sub>:183</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:185">a<sub>1</sub>:185</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:187">a<sub>1</sub>:187</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:189">a<sub>1</sub>:189</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Logic.html#a<sub>1</sub>:193">a<sub>1</sub>:193</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:4">a<sub>1</sub>:4</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:6">a<sub>1</sub>:6</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>1</sub>:8">a<sub>1</sub>:8</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Auto.html#a<sub>1</sub>:83">a<sub>1</sub>:83</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:119">a<sub>2</sub>:119</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:121">a<sub>2</sub>:121</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:123">a<sub>2</sub>:123</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:125">a<sub>2</sub>:125</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:13">a<sub>2</sub>:13</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:130">a<sub>2</sub>:130</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:134">a<sub>2</sub>:134</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:138">a<sub>2</sub>:138</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:142">a<sub>2</sub>:142</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:15">a<sub>2</sub>:15</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:150">a<sub>2</sub>:150</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:152">a<sub>2</sub>:152</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:154">a<sub>2</sub>:154</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:160">a<sub>2</sub>:160</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:164">a<sub>2</sub>:164</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:168">a<sub>2</sub>:168</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:17">a<sub>2</sub>:17</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:176">a<sub>2</sub>:176</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:178">a<sub>2</sub>:178</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:180">a<sub>2</sub>:180</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:184">a<sub>2</sub>:184</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:186">a<sub>2</sub>:186</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:188">a<sub>2</sub>:188</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:19">a<sub>2</sub>:19</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:190">a<sub>2</sub>:190</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Logic.html#a<sub>2</sub>:194">a<sub>2</sub>:194</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:5">a<sub>2</sub>:5</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:7">a<sub>2</sub>:7</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a<sub>2</sub>:9">a<sub>2</sub>:9</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Logic.html#A:10">A:10</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#A:105">A:105</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Imp.html#a:107">a:107</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a:109">a:109</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Logic.html#A:11">A:11</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Maps.html#A:11">A:11</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Logic.html#A:112">A:112</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="IndProp.html#a:112">a:112</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="ProofObjects.html#A:114">A:114</a> [binder, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="Logic.html#A:117">A:117</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#A:123">A:123</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#a:126">a:126</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#A:158">A:158</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Rel.html#a:16">a:16</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Maps.html#A:16">A:16</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="AltAuto.html#a:163">a:163</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#a:167">a:167</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#a:171">a:171</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Tactics.html#a:18">a:18</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Logic.html#A:186">A:186</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Rel.html#a:19">a:19</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Maps.html#A:19">A:19</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Logic.html#A:191">A:191</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Imp.html#a:195">a:195</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a:205">a:205</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a:222">a:222</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a:23">a:23</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Maps.html#A:23">A:23</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Tactics.html#a:28">a:28</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Maps.html#A:28">A:28</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Imp.html#a:285">a:285</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Rel.html#a:29">a:29</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Imp.html#a:29">a:29</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#a:32">a:32</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Rel.html#a:33">a:33</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Maps.html#A:33">A:33</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Tactics.html#a:34">a:34</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Logic.html#A:34">A:34</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Maps.html#A:36">A:36</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="IndProp.html#a:363">a:363</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:365">a:365</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:368">a:368</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#a:37">a:37</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndProp.html#a:375">a:375</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#a:38">a:38</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndProp.html#a:38">a:38</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:384">a:384</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:394">a:394</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:398">a:398</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:400">a:400</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#a:41">a:41</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Maps.html#A:42">A:42</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Maps.html#A:43">A:43</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Rel.html#A:44">A:44</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Imp.html#a:44">a:44</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Maps.html#A:44">A:44</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Maps.html#A:48">A:48</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Logic.html#A:5">A:5</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Maps.html#A:50">A:50</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Maps.html#A:54">A:54</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Rel.html#A:59">A:59</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Maps.html#A:59">A:59</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="ProofObjects.html#A:60">A:60</a> [binder, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="Poly.html#A:64">A:64</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="Maps.html#A:64">A:64</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Tactics.html#A:67">A:67</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="AltAuto.html#A:68">A:68</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Maps.html#A:68">A:68</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Auto.html#a:69">a:69</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Maps.html#A:74">A:74</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="AltAuto.html#A:75">A:75</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Maps.html#A:79">A:79</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Maps.html#A:8">A:8</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<a href="Tactics.html#a:85">a:85</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Maps.html#A:9">A:9</a> [binder, in <a href="Maps.html">Maps</a>]<br/>
<br/><br/><a id="global_B"></a><h2>B </h2>
<a href="Imp.html#BAnd">BAnd</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Tactics.html#bar">bar</a> [definition, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="IndPrinciples.html#base_case">base_case</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Basics.html#base:71">base:71</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html">Basics</a> [library]<br/>
<a href="Imp.html#BEq">BEq</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndPrinciples.html#better_t_tree_ind">better_t_tree_ind</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#better_t_tree_ind_type">better_t_tree_ind_type</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#beval">beval</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#bexp">bexp</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#bexp1">bexp1</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BFalse">BFalse</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BGt">BGt</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Bib.html">Bib</a> [library]<br/>
<a href="ImpParser.html#bignumber">bignumber</a> [definition, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="Basics.html#bin">bin</a> [inductive, in <a href="Basics.html">Basics</a>]<br/>
<a href="Induction.html#bin">bin</a> [inductive, in <a href="Induction.html">Induction</a>]<br/>
<a href="Basics.html#bin_to_nat">bin_to_nat</a> [definition, in <a href="Basics.html">Basics</a>]<br/>
<a href="Induction.html#bin_nat_bin">bin_nat_bin</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#bin_nat_bin_fails">bin_nat_bin_fails</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#bin_nat_bin_fails">bin_nat_bin_fails</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#bin_to_nat_pres_incr">bin_to_nat_pres_incr</a> [lemma, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#bin_to_nat">bin_to_nat</a> [definition, in <a href="Induction.html">Induction</a>]<br/>
<a href="IndProp.html#bin1">bin1</a> [module, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin1.bin">bin1.bin</a> [inductive, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin1.B0">bin1.B0</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin1.B1">bin1.B1</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin1.Z">bin1.Z</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin2">bin2</a> [module, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin2.bin">bin2.bin</a> [inductive, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin2.B0">bin2.B0</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin2.B1">bin2.B1</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin2.Z">bin2.Z</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin3">bin3</a> [module, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin3.bin">bin3.bin</a> [inductive, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin3.B0">bin3.B0</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin3.B1">bin3.B1</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#bin3.Z">bin3.Z</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Basics.html#black">black</a> [constructor, in <a href="Basics.html">Basics</a>]<br/>
<a href="Imp.html#BLe">BLe</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#blue">blue</a> [constructor, in <a href="Basics.html">Basics</a>]<br/>
<a href="IndPrinciples.html#blue">blue</a> [constructor, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#BNeq">BNeq</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BNot">BNot</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#bool">bool</a> [inductive, in <a href="Basics.html">Basics</a>]<br/>
<a href="Poly.html#boollist">boollist</a> [inductive, in <a href="Poly.html">Poly</a>]<br/>
<a href="IndPrinciples.html#booltree">booltree</a> [inductive, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#booltree_ind_type_correct">booltree_ind_type_correct</a> [lemma, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#booltree_ind_type">booltree_ind_type</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#booltree_property_type">booltree_property_type</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Tactics.html#bool_fn_applied_thrice">bool_fn_applied_thrice</a> [lemma, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Poly.html#bool_cons">bool_cons</a> [constructor, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#bool_nil">bool_nil</a> [constructor, in <a href="Poly.html">Poly</a>]<br/>
<a href="IndPrinciples.html#branch_case">branch_case</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#BreakImp">BreakImp</a> [module, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.break_ignore">BreakImp.break_ignore</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.CAsgn">BreakImp.CAsgn</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.CBreak">BreakImp.CBreak</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.ceval">BreakImp.ceval</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.ceval_deterministic">BreakImp.ceval_deterministic</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.CIf">BreakImp.CIf</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.com">BreakImp.com</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.CSeq">BreakImp.CSeq</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.CSkip">BreakImp.CSkip</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.CWhile">BreakImp.CWhile</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.E_Skip">BreakImp.E_Skip</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.result">BreakImp.result</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.SBreak">BreakImp.SBreak</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.SContinue">BreakImp.SContinue</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.seq_stops_on_break">BreakImp.seq_stops_on_break</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.seq_continue">BreakImp.seq_continue</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.while_break_true">BreakImp.while_break_true</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.while_stops_on_break">BreakImp.while_stops_on_break</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.while_continue">BreakImp.while_continue</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.:com:com_scope:'while'_x_'do'_x_'end'">com:while _ do _ end (com_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.:com:com_scope:'if'_x_'then'_x_'else'_x_'end'">com:if _ then _ else _ end (com_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#9693f1fd6e0ff7b00e2ee85219ea9702">com:_ ; _ (com_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#6bf84ee0220c3a3f4df8e9da0b95f172">com:_ := _ (com_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.:com:com_scope:'skip'">com:skip (com_scope)</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BreakImp.:com::'break'">com:break</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#2b326eb0d5dcd2404a8e7abc4d2a6400">_ =[ _ ]=> _ / _</a> [notation, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#BTrue">BTrue</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndPrinciples.html#bt_branch">bt_branch</a> [constructor, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#bt_leaf">bt_leaf</a> [constructor, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#bt_empty">bt_empty</a> [constructor, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndPrinciples.html#build_proof">build_proof</a> [definition, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#bv:114">bv:114</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#B<sub>0</sub>">B<sub>0</sub></a> [constructor, in <a href="Basics.html">Basics</a>]<br/>
<a href="Induction.html#B<sub>0</sub>">B<sub>0</sub></a> [constructor, in <a href="Induction.html">Induction</a>]<br/>
<a href="Basics.html#b<sub>0</sub>:38">b<sub>0</sub>:38</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#B<sub>1</sub>">B<sub>1</sub></a> [constructor, in <a href="Basics.html">Basics</a>]<br/>
<a href="Induction.html#B<sub>1</sub>">B<sub>1</sub></a> [constructor, in <a href="Induction.html">Induction</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:12">b<sub>1</sub>:12</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:16">b<sub>1</sub>:16</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:18">b<sub>1</sub>:18</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Logic.html#b<sub>1</sub>:180">b<sub>1</sub>:180</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#b<sub>1</sub>:182">b<sub>1</sub>:182</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Imp.html#b<sub>1</sub>:192">b<sub>1</sub>:192</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:20">b<sub>1</sub>:20</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Imp.html#b<sub>1</sub>:21">b<sub>1</sub>:21</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:22">b<sub>1</sub>:22</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:39">b<sub>1</sub>:39</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>1</sub>:9">b<sub>1</sub>:9</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:10">b<sub>2</sub>:10</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:13">b<sub>2</sub>:13</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:17">b<sub>2</sub>:17</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Logic.html#b<sub>2</sub>:181">b<sub>2</sub>:181</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#b<sub>2</sub>:183">b<sub>2</sub>:183</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:19">b<sub>2</sub>:19</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Imp.html#b<sub>2</sub>:193">b<sub>2</sub>:193</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:21">b<sub>2</sub>:21</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Imp.html#b<sub>2</sub>:22">b<sub>2</sub>:22</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:23">b<sub>2</sub>:23</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>2</sub>:40">b<sub>2</sub>:40</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>3</sub>:24">b<sub>3</sub>:24</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b<sub>3</sub>:41">b<sub>3</sub>:41</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Auto.html#b:101">b:101</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Basics.html#b:105">b:105</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b:106">b:106</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Auto.html#b:107">b:107</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Basics.html#b:108">b:108</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b:110">b:110</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Auto.html#b:111">b:111</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Imp.html#b:113">b:113</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Basics.html#b:113">b:113</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Logic.html#B:113">B:113</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="IndProp.html#b:113">b:113</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Auto.html#b:116">b:116</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Basics.html#b:116">b:116</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Logic.html#B:118">B:118</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#B:12">B:12</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Basics.html#b:125">b:125</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Basics.html#b:126">b:126</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="AltAuto.html#b:13">b:13</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Tactics.html#b:132">b:132</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Basics.html#b:15">b:15</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Poly.html#b:160">b:160</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="AltAuto.html#b:164">b:164</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:168">b:168</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:172">b:172</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:177">b:177</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:178">b:178</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:181">b:181</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:182">b:182</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:184">b:184</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:187">b:187</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#b:189">b:189</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Tactics.html#b:19">b:19</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Imp.html#b:191">b:191</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="AltAuto.html#b:191">b:191</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Imp.html#b:199">b:199</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Rel.html#b:20">b:20</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Imp.html#b:20">b:20</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:208">b:208</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:211">b:211</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Logic.html#b:227">b:227</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Imp.html#b:232">b:232</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:237">b:237</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:240">b:240</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:246">b:246</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:26">b:26</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:288">b:288</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Tactics.html#b:29">b:29</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Imp.html#b:291">b:291</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Poly.html#b:3">b:3</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="Rel.html#b:30">b:30</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="IndPrinciples.html#b:30">b:30</a> [binder, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#b:302">b:302</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#b:307">b:307</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndPrinciples.html#b:31">b:31</a> [binder, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndProp.html#b:311">b:311</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#b:313">b:313</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#b:320">b:320</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Rel.html#b:34">b:34</a> [binder, in <a href="Rel.html">Rel</a>]<br/>
<a href="Tactics.html#b:35">b:35</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Logic.html#B:35">B:35</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="IndProp.html#b:366">b:366</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndPrinciples.html#b:38">b:38</a> [binder, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="IndProp.html#b:39">b:39</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#b:41">b:41</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndProp.html#b:42">b:42</a> [binder, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#b:43">b:43</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="IndPrinciples.html#b:44">b:44</a> [binder, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#b:45">b:45</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Induction.html#b:45">b:45</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#b:48">b:48</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Logic.html#b:53">b:53</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#b:54">b:54</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#B:6">B:6</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#b:62">b:62</a> [binder, in <a href="Logic.html">Logic</a>]<br/>
<a href="Induction.html#b:67">b:67</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Tactics.html#B:68">B:68</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="AltAuto.html#B:69">B:69</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Basics.html#b:7">b:7</a> [binder, in <a href="Basics.html">Basics</a>]<br/>
<a href="Induction.html#b:71">b:71</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Auto.html#b:72">b:72</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Induction.html#b:73">b:73</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#b:74">b:74</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Auto.html#b:75">b:75</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Induction.html#b:75">b:75</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Induction.html#b:76">b:76</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="AltAuto.html#B:76">B:76</a> [binder, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Tactics.html#b:78">b:78</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Auto.html#b:78">b:78</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Induction.html#b:78">b:78</a> [binder, in <a href="Induction.html">Induction</a>]<br/>
<a href="Tactics.html#b:86">b:86</a> [binder, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Auto.html#b:93">b:93</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#b:98">b:98</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<br/><br/><a id="global_C"></a><h2>C </h2>
<a href="IndProp.html#c">c</a> [definition, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#CAsgn">CAsgn</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#ceval">ceval</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#ceval_deterministic">ceval_deterministic</a> [lemma, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#ceval_example2">ceval_example2</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#ceval_example1">ceval_example1</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#ceval_fun_no_while">ceval_fun_no_while</a> [definition, in <a href="Imp.html">Imp</a>]<br/>
<a href="Auto.html#ceval_example1">ceval_example1</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#ceval_deterministic''''">ceval_deterministic''''</a> [lemma, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#ceval_deterministic'''">ceval_deterministic'''</a> [lemma, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#ceval_deterministic''">ceval_deterministic''</a> [lemma, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#ceval_deterministic'_alt">ceval_deterministic'_alt</a> [lemma, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#ceval_deterministic'">ceval_deterministic'</a> [lemma, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#ceval_deterministic">ceval_deterministic</a> [lemma, in <a href="Auto.html">Auto</a>]<br/>
<a href="ImpCEvalFun.html#ceval_deterministic'">ceval_deterministic'</a> [lemma, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_and_ceval_step_coincide">ceval_and_ceval_step_coincide</a> [lemma, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval__ceval_step">ceval__ceval_step</a> [lemma, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_step_more">ceval_step_more</a> [lemma, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_step__ceval">ceval_step__ceval</a> [lemma, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_step">ceval_step</a> [definition, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_step3">ceval_step3</a> [definition, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_step2">ceval_step2</a> [definition, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="ImpCEvalFun.html#ceval_step1">ceval_step1</a> [definition, in <a href="ImpCEvalFun.html">ImpCEvalFun</a>]<br/>
<a href="Auto.html#ceval'_example1">ceval'_example1</a> [definition, in <a href="Auto.html">Auto</a>]<br/>
<a href="IndProp.html#Char">Char</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="ImpParser.html#chartype">chartype</a> [inductive, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="IndProp.html#char_eps_suffix">char_eps_suffix</a> [lemma, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#char_nomatch_char">char_nomatch_char</a> [lemma, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#Chf_more">Chf_more</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#Chf_done">Chf_done</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Imp.html#CIf">CIf</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="ImpParser.html#classifyChar">classifyChar</a> [definition, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="IndProp.html#Cleo">Cleo</a> [constructor, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Rel.html#clos_refl_trans_1n">clos_refl_trans_1n</a> [inductive, in <a href="Rel.html">Rel</a>]<br/>
<a href="Rel.html#clos_refl_trans">clos_refl_trans</a> [inductive, in <a href="Rel.html">Rel</a>]<br/>
<a href="IndProp.html#clos_trans">clos_trans</a> [inductive, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="ImpParser.html#cls:16">cls:16</a> [binder, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="IndProp.html#collatz">collatz</a> [axiom, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#Collatz_holds_for_12">Collatz_holds_for_12</a> [definition, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="IndProp.html#Collatz_holds_for">Collatz_holds_for</a> [inductive, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Basics.html#color">color</a> [inductive, in <a href="Basics.html">Basics</a>]<br/>
<a href="Imp.html#com">com</a> [inductive, in <a href="Imp.html">Imp</a>]<br/>
<a href="Poly.html#combine">combine</a> [definition, in <a href="Poly.html">Poly</a>]<br/>
<a href="Tactics.html#combine_split">combine_split</a> [lemma, in <a href="Tactics.html">Tactics</a>]<br/>
<a href="Logic.html#combine_odd_even_elim_even">combine_odd_even_elim_even</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#combine_odd_even_elim_odd">combine_odd_even_elim_odd</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#combine_odd_even_intro">combine_odd_even_intro</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#combine_odd_even">combine_odd_even</a> [definition, in <a href="Logic.html">Logic</a>]<br/>
<a href="Poly.html#cons">cons</a> [constructor, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#constfun">constfun</a> [definition, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#constfun_example2">constfun_example2</a> [definition, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#constfun_example1">constfun_example1</a> [definition, in <a href="Poly.html">Poly</a>]<br/>
<a href="AltAuto.html#constructor_example">constructor_example</a> [definition, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="Poly.html#cons'">cons'</a> [constructor, in <a href="Poly.html">Poly</a>]<br/>
<a href="ProofObjects.html#contradiction_implies_anything">contradiction_implies_anything</a> [definition, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="Logic.html#contradiction_implies_anything">contradiction_implies_anything</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="Logic.html#contrapositive">contrapositive</a> [lemma, in <a href="Logic.html">Logic</a>]<br/>
<a href="AltAuto.html#contras">contras</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="AltAuto.html#contras'">contras'</a> [lemma, in <a href="AltAuto.html">AltAuto</a>]<br/>
<a href="ProofObjects.html#contra:74">contra:74</a> [binder, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="IndProp.html#count">count</a> [definition, in <a href="IndProp.html">IndProp</a>]<br/>
<a href="Poly.html#countoddmembers'">countoddmembers'</a> [definition, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#count:14">count:14</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="Lists.html#count:26">count:26</a> [binder, in <a href="Lists.html">Lists</a>]<br/>
<a href="Poly.html#count:28">count:28</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#count:35">count:35</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="Poly.html#count:40">count:40</a> [binder, in <a href="Poly.html">Poly</a>]<br/>
<a href="Imp.html#CSeq">CSeq</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#CSkip">CSkip</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="ProofObjects.html#curry">curry</a> [definition, in <a href="ProofObjects.html">ProofObjects</a>]<br/>
<a href="Imp.html#CWhile">CWhile</a> [constructor, in <a href="Imp.html">Imp</a>]<br/>
<a href="ImpParser.html#c':174">c':174</a> [binder, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="ImpParser.html#c':186">c':186</a> [binder, in <a href="ImpParser.html">ImpParser</a>]<br/>
<a href="IndPrinciples.html#C<sub>1</sub>">C<sub>1</sub></a> [constructor, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:206">c<sub>1</sub>:206</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:209">c<sub>1</sub>:209</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:225">c<sub>1</sub>:225</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:233">c<sub>1</sub>:233</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:238">c<sub>1</sub>:238</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:286">c<sub>1</sub>:286</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:289">c<sub>1</sub>:289</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:311">c<sub>1</sub>:311</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>1</sub>:316">c<sub>1</sub>:316</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Auto.html#c<sub>1</sub>:70">c<sub>1</sub>:70</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>1</sub>:73">c<sub>1</sub>:73</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>1</sub>:86">c<sub>1</sub>:86</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>1</sub>:94">c<sub>1</sub>:94</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>1</sub>:99">c<sub>1</sub>:99</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="IndPrinciples.html#C<sub>2</sub>">C<sub>2</sub></a> [constructor, in <a href="IndPrinciples.html">IndPrinciples</a>]<br/>
<a href="Auto.html#c<sub>2</sub>:100">c<sub>2</sub>:100</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:207">c<sub>2</sub>:207</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:210">c<sub>2</sub>:210</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:226">c<sub>2</sub>:226</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:234">c<sub>2</sub>:234</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:239">c<sub>2</sub>:239</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:287">c<sub>2</sub>:287</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:290">c<sub>2</sub>:290</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:312">c<sub>2</sub>:312</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Imp.html#c<sub>2</sub>:317">c<sub>2</sub>:317</a> [binder, in <a href="Imp.html">Imp</a>]<br/>
<a href="Auto.html#c<sub>2</sub>:71">c<sub>2</sub>:71</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>2</sub>:74">c<sub>2</sub>:74</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>2</sub>:87">c<sub>2</sub>:87</a> [binder, in <a href="Auto.html">Auto</a>]<br/>
<a href="Auto.html#c<sub>2</sub>:95">c<sub>2</sub>:95</a> [binder, in <a href="Auto.html">Auto</a>]<br/>