FSafe.List
R163 Coq.Lists.List nil
R191 Coq.Lists.List cons
R198 Coq.Lists.List nil
R236 Coq.Lists.List cons
R247 Coq.Lists.List cons
R254 Coq.Lists.List nil
FSafe.List
R154 Coq.Lists.List nil
R182 Coq.Lists.List cons
R189 Coq.Lists.List nil
R227 Coq.Lists.List cons
R238 Coq.Lists.List cons
R245 Coq.Lists.List nil
R-1 Coq.Init.Specif sig
R387 Coq.Init.Logic "x <> y" type_scope
R378 Coq.Lists.List length
R390 Coq.Init.Datatypes "" nat_scope
R369 Coq.Lists.List list
R443 Coq.Lists.List nil
R450 Coq.Program.Utils " ! "
R465 Coq.Lists.List "x :: y" list_scope
R735 Coq.Lists.List list
R-1 Coq.Init.Specif sig
R727 Coq.Init.Logic "x <> y" type_scope
R718 Coq.Lists.List length
R730 Coq.Init.Datatypes "" nat_scope
R709 Coq.Lists.List list
R770 Coq.Lists.List nil
R777 Coq.Program.Utils " ! "
R790 Coq.Lists.List "x :: y" list_scope
R-1 Coq.Init.Specif sig
R727 Coq.Init.Logic "x <> y" type_scope
R718 Coq.Lists.List length
R730 Coq.Init.Datatypes "" nat_scope
R709 Coq.Lists.List list
R849 Coq.Lists.List list
R859 Safe.List Accessors.tail
R864 Coq.Lists.List nil
R-1 Coq.Init.Specif sig
R931 Coq.Init.Logic "x <> y" type_scope
R934 Coq.Lists.List nil
R920 Coq.Lists.List list
R948 Coq.Lists.List length
R989 Coq.Lists.List nil
R996 Coq.Program.Utils " ! "
R1009 Coq.Lists.List "x :: y" list_scope
R1012 Coq.Lists.List nil
R1033 Coq.Lists.List "x :: y" list_scope
R-1 Coq.Init.Specif sig
R1213 Coq.Init.Logic "x <> y" type_scope
R1204 Coq.Lists.List length
R1216 Coq.Init.Datatypes "" nat_scope
R1195 Coq.Lists.List list
R1228 Coq.Lists.List length
R1238 Coq.Lists.List list
R1238 Coq.Lists.List list
R1274 Coq.Lists.List nil
R1281 Coq.Program.Utils " ! "
R1294 Coq.Lists.List "x :: y" list_scope
R1297 Coq.Lists.List nil
R1304 Coq.Lists.List nil
R1319 Coq.Lists.List "x :: y" list_scope
R1325 Coq.Lists.List "x :: y" list_scope
R1343 Coq.Lists.List "x :: y" list_scope
R1409 Coq.Init.Datatypes nat
R1416 Safe.List head
R1422 Coq.Lists.List cons
R1429 Coq.Lists.List nil
R1427 Coq.Init.Datatypes "" nat_scope
R1451 Safe.List test_hd
R1544 Coq.Lists.List list
R1549 Coq.Init.Datatypes nat
R1556 Safe.List liat
R1562 Safe.List " [ x ; .. ; y ] "
R1571 Coq.Init.Datatypes "" nat_scope
R1567 Coq.Init.Datatypes "" nat_scope
R1563 Coq.Init.Datatypes "" nat_scope
R1589 Safe.List test_liat
R1632 Coq.Lists.List list
R1637 Coq.Init.Datatypes nat
R1644 Safe.List tail
R1650 Safe.List " [ x ; .. ; y ] "
R1659 Coq.Init.Datatypes "" nat_scope
R1655 Coq.Init.Datatypes "" nat_scope
R1651 Coq.Init.Datatypes "" nat_scope
R1677 Safe.List test_tail
R1794 Coq.Init.Specif "{ x : A  |  P }" type_scope
R1818 Coq.Init.Logic "x = y" type_scope
R1809 Coq.Lists.List length
R1829 Coq.Init.Peano "n + m" nat_scope
R1820 Coq.Lists.List length
R1831 Coq.Lists.List length
R1800 Coq.Lists.List list
R1767 Coq.Lists.List list
R1753 Coq.Lists.List list
R1871 Coq.Lists.List nil
R1892 Coq.Lists.List "x :: y" list_scope
R1904 Coq.Lists.List "x :: y" list_scope
R1911 Safe.List "x ++ y"
R1767 Coq.Lists.List list
R1753 Coq.Lists.List list
R2093 Coq.Init.Logic "x = y" type_scope
R2099 Coq.Lists.List "x ++ y" list_scope
R2095 Coq.Lists.List nil
R2083 Coq.Lists.List list
R2190 Coq.Init.Logic "x = y" type_scope
R2194 Coq.Lists.List "x ++ y" list_scope
R2197 Coq.Lists.List nil
R2180 Coq.Lists.List list
R-1 Coq.Init.Specif sig
R2373 Coq.Init.Peano "x < y" nat_scope
R2375 Coq.Lists.List length
R2365 Coq.Init.Datatypes nat
R2352 Coq.Lists.List list
R2434 Coq.Init.Datatypes "" nat_scope
R2440 Coq.Lists.List "x :: y" list_scope
R2459 Coq.Init.Datatypes S
R2467 Coq.Lists.List "x :: y" list_scope
R2497 Coq.Lists.List nil
R2504 Coq.Program.Utils " ! "
R-1 Coq.Init.Specif sig
R2373 Coq.Init.Peano "x < y" nat_scope
R2375 Coq.Lists.List length
R2365 Coq.Init.Datatypes nat
R2352 Coq.Lists.List list
R2651 Coq.Init.Specif "{ x : A  |  P }" type_scope
R2668 Coq.Init.Logic "x <> y" type_scope
R2671 Coq.Lists.List nil
R2657 Coq.Lists.List list
R2681 Coq.Lists.List cons
R2688 Coq.Lists.List nil
R2764 Coq.Lists.List list
R2976 Coq.Init.Specif sig
R2987 Coq.Lists.List "x ++ y" list_scope
R2949 Coq.Init.Specif sig
R2919 Coq.Init.Specif sig
R2930 Coq.Lists.List "x ++ y" list_scope
R2933 Safe.List " [ x ; .. ; y ] "
R2905 Coq.Init.Specif sig
R2896 Coq.Lists.List list
R2870 Coq.Init.Specif "{ x : A  |  P }" type_scope
R2880 Coq.Lists.List In
R2841 Coq.Lists.List list
R2827 Coq.Lists.List list
R3022 Safe.List " [] "
R3041 Coq.Lists.List "x :: y" list_scope
R2949 Coq.Init.Specif sig
R2919 Coq.Init.Specif sig
R2930 Coq.Lists.List "x ++ y" list_scope
R2933 Safe.List " [ x ; .. ; y ] "
R2905 Coq.Init.Specif sig
R2896 Coq.Lists.List list
R2870 Coq.Init.Specif "{ x : A  |  P }" type_scope
R2880 Coq.Lists.List In
R2841 Coq.Lists.List list
R2827 Coq.Lists.List list
R3350 Coq.Lists.List app_ass
R3350 Coq.Lists.List app_ass
R3570 Coq.Init.Specif sig
R3556 Coq.Init.Specif sig
R3563 Safe.List " [] "
R3526 Coq.Init.Specif sig
R3537 Coq.Lists.List "x ++ y" list_scope
R3540 Safe.List " [ x ; .. ; y ] "
R3512 Coq.Init.Specif sig
R3503 Coq.Lists.List list
R3477 Coq.Init.Specif "{ x : A  |  P }" type_scope
R3487 Coq.Lists.List In
R3448 Coq.Lists.List list
R3588 Safe.List Fold_Left.fold_left_aux
R3604 Safe.List " [] "
R3556 Coq.Init.Specif sig
R3563 Safe.List " [] "
R3526 Coq.Init.Specif sig
R3537 Coq.Lists.List "x ++ y" list_scope
R3540 Safe.List " [ x ; .. ; y ] "
R3512 Coq.Init.Specif sig
R3503 Coq.Lists.List list
R3477 Coq.Init.Specif "{ x : A  |  P }" type_scope
R3487 Coq.Lists.List In
R3448 Coq.Lists.List list
R3690 Coq.Lists.List list
R3889 Coq.Init.Specif sig
R3862 Coq.Init.Specif sig
R3869 Safe.List " [] "
R3834 Coq.Init.Specif sig
R3844 Coq.Lists.List "x :: y" list_scope
R3813 Coq.Init.Specif "{ x : A  |  P }" type_scope
R3823 Coq.Lists.List In
R3787 Coq.Init.Specif sig
R3778 Coq.Lists.List list
R3748 Coq.Lists.List list
R3927 Safe.List " [] "
R3946 Coq.Lists.List "x :: y" list_scope
R3862 Coq.Init.Specif sig
R3869 Safe.List " [] "
R3834 Coq.Init.Specif sig
R3844 Coq.Lists.List "x :: y" list_scope
R3813 Coq.Init.Specif "{ x : A  |  P }" type_scope
R3823 Coq.Lists.List In
R3787 Coq.Init.Specif sig
R3778 Coq.Lists.List list
R3748 Coq.Lists.List list