CristalCaveGem » LustreC

(* Frama-C journal generated at 17:03 the 17/02/2015 *)

exception Unreachable

exception Exception of string

(* Run the user commands *)

let run () = ()

(* Main *)

let main () =

  Journal.keep_file "./.frama-c/frama_c_journal.ml";

  try run ()

  with

  | Unreachable -> Kernel.fatal "Journal reaches an assumed dead code" 

  | Exception s -> Kernel.log "Journal re-raised the exception %S" s

  | exn ->

    Kernel.fatal

      "Journal raised an unexpected exception: %s"

      (Printexc.to_string exn)

(* Registering *)

let main : unit -> unit =

  Dynamic.register

    ~plugin:"Frama_c_journal.ml"

    "main"

    (Datatype.func Datatype.unit Datatype.unit)

    ~journalize:false

    main

(* Hooking *)

let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()

DIGEST a67e786cf59f0f9bb308946312df06f5

FStreamsLib

R15:21 Coq.Lists.Streams <> <> lib

R32:35 Coq.Lists.List <> <> lib

R53:58 Coq.Setoids.Setoid <> <> lib

R76:95 Coq.Relations.Relation_Definitions <> <> lib

R113:122 Coq.Program.Wf <> <> lib

R140:145 Coq.Arith.Wf_nat <> <> lib

R163:173 Coq.Wellfounded.Wellfounded <> <> lib

def 188:191 <> mapT

R243:243 StreamsLib <> F var

R245:245 StreamsLib <> B var

R234:234 StreamsLib <> F var

R236:236 StreamsLib <> A var

R227:227 StreamsLib <> B var

R222:222 StreamsLib <> A var

def 261:266 <> applyT

R322:322 StreamsLib <> F var

R324:324 StreamsLib <> B var

R313:313 StreamsLib <> F var

R315:315 StreamsLib <> A var

R297:297 StreamsLib <> F var

R305:305 StreamsLib <> B var

R300:300 StreamsLib <> A var

def 340:351 <> option_apply

R362:367 StreamsLib <> applyT def

R378:378 StreamsLib <> B var

R376:376 StreamsLib <> A var

R369:374 Coq.Init.Datatypes <> option ind

R405:405 StreamsLib <> a var

R402:402 StreamsLib <> f var

R415:418 Coq.Init.Datatypes <> Some constr

R423:426 Coq.Init.Datatypes <> Some constr

R433:436 Coq.Init.Datatypes <> Some constr

R439:439 StreamsLib <> f var

R441:441 StreamsLib <> a var

R465:468 Coq.Init.Datatypes <> None constr

ax 484:490 <> eqst_eq

R513:518 Coq.Lists.Streams <> Stream coind

R520:520 StreamsLib <> A var

R538:540 Coq.Init.Logic <> :type_scope:x_'='_x not

R537:537 StreamsLib <> s var

R541:542 StreamsLib <> s' var

R524:527 Coq.Lists.Streams <> EqSt coind

R531:532 StreamsLib <> s' var

R529:529 StreamsLib <> s var

prf 554:560 <> inv_inv

R580:585 Coq.Lists.Streams <> Stream coind

R587:587 StreamsLib <> A var

R603:608 Coq.Lists.Streams <> Stream coind

R610:610 StreamsLib <> A var

R628:633 Coq.Lists.Streams <> ForAll coind

R659:659 StreamsLib <> s var

R646:651 Coq.Lists.Streams <> ForAll coind

R655:656 StreamsLib <> s' var

R653:653 StreamsLib <> P var

R614:619 Coq.Lists.Streams <> ForAll coind

R623:623 StreamsLib <> s var

R621:621 StreamsLib <> P var

R733:746 Coq.Lists.Streams <> HereAndFurther constr

R733:746 Coq.Lists.Streams <> HereAndFurther constr

prf 823:829 <> evt_inv

R851:856 Coq.Lists.Streams <> Stream coind

R858:858 StreamsLib <> A var

R874:879 Coq.Lists.Streams <> Stream coind

R881:881 StreamsLib <> A var

R915:920 Coq.Lists.Streams <> Exists ind

R947:947 StreamsLib <> s var

R937:940 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R933:933 StreamsLib <> P var

R935:936 StreamsLib <> s' var

R941:941 StreamsLib <> Q var

R943:944 StreamsLib <> s' var

R901:906 Coq.Lists.Streams <> Exists ind

R910:910 StreamsLib <> s var

R908:908 StreamsLib <> Q var

R887:892 Coq.Lists.Streams <> ForAll coind

R896:896 StreamsLib <> s var

R894:894 StreamsLib <> P var

R977:980 Coq.Lists.Streams <> Here constr

R977:980 Coq.Lists.Streams <> Here constr

R0:-1 StreamsLib <> y var

R1017:1023 Coq.Lists.Streams <> Further constr

R1017:1023 Coq.Lists.Streams <> Further constr

def 1087:1098 <> ForAll_apply

R1112:1117 Coq.Lists.Streams <> Stream coind

R1119:1119 StreamsLib <> A var

R1196:1201 Coq.Lists.Streams <> ForAll coind

R1205:1205 StreamsLib <> s var

R1203:1203 StreamsLib <> Q var

R1160:1165 Coq.Lists.Streams <> ForAll coind

R1189:1189 StreamsLib <> s var

R1184:1184 StreamsLib <> Q var

R1186:1186 StreamsLib <> s var

R1177:1177 StreamsLib <> P var

R1179:1179 StreamsLib <> s var

R1144:1149 Coq.Lists.Streams <> ForAll coind

R1153:1153 StreamsLib <> s var

R1151:1151 StreamsLib <> P var

R1257:1265 StreamsLib <> always_pq var

R1247:1254 StreamsLib <> always_p var

R1276:1289 Coq.Lists.Streams <> HereAndFurther constr

R1308:1321 Coq.Lists.Streams <> HereAndFurther constr

R1343:1356 Coq.Lists.Streams <> HereAndFurther constr

R1372:1383 StreamsLib <> ForAll_apply def

R1386:1387 Coq.Lists.Streams <> tl def

R1389:1389 StreamsLib <> s var

R1358:1358 StreamsLib <> s var

def 1432:1444 <> necessitation

R1455:1460 Coq.Lists.Streams <> Stream coind

R1462:1462 StreamsLib <> A var

R1488:1488 StreamsLib <> P var

R1490:1490 StreamsLib <> s var

R1497:1502 Coq.Lists.Streams <> ForAll coind

R1506:1506 StreamsLib <> s var

R1504:1504 StreamsLib <> P var

R1512:1525 Coq.Lists.Streams <> HereAndFurther constr

R1536:1548 StreamsLib <> necessitation def

R1553:1554 Coq.Lists.Streams <> tl def

R1556:1556 StreamsLib <> s var

R1550:1550 StreamsLib <> I var

R1530:1530 StreamsLib <> I var

R1532:1532 StreamsLib <> s var

R1527:1527 StreamsLib <> s var

def 1573:1588 <> ForAll_reinforce

R1602:1607 Coq.Lists.Streams <> Stream coind

R1609:1609 StreamsLib <> A var

R1670:1675 Coq.Lists.Streams <> ForAll coind

R1679:1679 StreamsLib <> s var

R1677:1677 StreamsLib <> Q var

R1634:1639 Coq.Lists.Streams <> ForAll coind

R1663:1663 StreamsLib <> s var

R1654:1657 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R1651:1651 StreamsLib <> P var

R1653:1653 StreamsLib <> s var

R1658:1658 StreamsLib <> Q var

R1660:1660 StreamsLib <> s var

R1705:1716 StreamsLib <> ForAll_apply def

R1705:1716 StreamsLib <> ForAll_apply def

R1737:1749 StreamsLib <> necessitation def

R1737:1749 StreamsLib <> necessitation def

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

def 1785:1790 <> concat

R1806:1809 Coq.Init.Datatypes <> list ind

R1811:1811 StreamsLib <> A var

R1824:1829 Coq.Lists.Streams <> Stream coind

R1831:1831 StreamsLib <> A var

R1836:1841 Coq.Lists.Streams <> Stream coind

R1843:1843 StreamsLib <> A var

R1849:1862 Coq.Lists.List <> fold_left def

R1893:1898 StreamsLib <> suffix var

R1886:1891 StreamsLib <> prefix var

R1876:1879 Coq.Lists.Streams <> Cons constr

R1883:1883 StreamsLib <> q var

R1881:1881 StreamsLib <> t var

prf 1910:1920 <> eqst_concat

R1951:1956 Coq.Lists.Streams <> Stream coind

R1958:1958 StreamsLib <> A var

R1979:1982 Coq.Lists.Streams <> EqSt coind

R2002:2007 StreamsLib <> concat def

R2013:2016 StreamsLib <> sfx' var

R2009:2011 StreamsLib <> pfx var

R1985:1990 StreamsLib <> concat def

R1996:1998 StreamsLib <> sfx var

R1992:1994 StreamsLib <> pfx var

R1962:1965 Coq.Lists.Streams <> EqSt coind

R1971:1974 StreamsLib <> sfx' var

R1967:1969 StreamsLib <> sfx var

R2088:2091 Coq.Lists.Streams <> eqst constr

R2088:2091 Coq.Lists.Streams <> eqst constr

prf 2135:2145 <> concat_eqst

R2181:2186 Coq.Lists.Streams <> Stream coind

R2188:2188 StreamsLib <> A var

R2284:2287 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R2277:2279 Coq.Init.Logic <> :type_scope:x_'='_x not

R2274:2276 StreamsLib <> pfx var

R2280:2283 StreamsLib <> pfx' var

R2288:2291 Coq.Lists.Streams <> EqSt coind

R2297:2300 StreamsLib <> sfx' var

R2293:2295 StreamsLib <> sfx var

R2230:2233 Coq.Lists.Streams <> EqSt coind

R2253:2258 StreamsLib <> concat def

R2265:2268 StreamsLib <> sfx' var

R2260:2263 StreamsLib <> pfx' var

R2236:2241 StreamsLib <> concat def

R2247:2249 StreamsLib <> sfx var

R2243:2245 StreamsLib <> pfx var

R2207:2209 Coq.Init.Logic <> :type_scope:x_'='_x not

R2192:2202 Coq.Lists.List <> length syndef

R2204:2206 StreamsLib <> pfx var

R2210:2220 Coq.Lists.List <> length syndef

R2222:2225 StreamsLib <> pfx' var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

prf 2588:2593 <> evt_id

R2613:2618 Coq.Lists.Streams <> Stream coind

R2620:2620 StreamsLib <> A var

R2624:2629 Coq.Lists.Streams <> Exists ind

R2650:2650 StreamsLib <> s var

R2643:2645 Coq.Init.Logic <> :type_scope:x_'='_x not

R2642:2642 StreamsLib <> s var

R2646:2647 StreamsLib <> s' var

R2674:2677 Coq.Lists.Streams <> Here constr

R2674:2677 Coq.Lists.Streams <> Here constr

prf 2707:2716 <> evt_concat

R2736:2741 Coq.Lists.Streams <> Stream coind

R2743:2743 StreamsLib <> A var

R2761:2766 Coq.Lists.Streams <> Stream coind

R2768:2768 StreamsLib <> A var

R2786:2791 Coq.Lists.Streams <> Exists ind

R2796:2801 StreamsLib <> concat def

R2805:2805 StreamsLib <> s var

R2803:2803 StreamsLib <> p var

R2793:2793 StreamsLib <> P var

R2772:2777 Coq.Lists.Streams <> Exists ind

R2781:2781 StreamsLib <> s var

R2779:2779 StreamsLib <> P var

R2866:2869 Coq.Lists.Streams <> Cons constr

R2866:2869 Coq.Lists.Streams <> Cons constr

R2885:2891 Coq.Lists.Streams <> Further constr

R2885:2891 Coq.Lists.Streams <> Further constr

prf 2918:2927 <> inv_concat

R2947:2952 Coq.Lists.Streams <> Stream coind

R2954:2954 StreamsLib <> A var

R2972:2977 Coq.Lists.Streams <> Stream coind

R2979:2979 StreamsLib <> A var

R3008:3013 Coq.Lists.Streams <> ForAll coind

R3017:3017 StreamsLib <> s var

R3015:3015 StreamsLib <> P var

R2983:2988 Coq.Lists.Streams <> ForAll coind

R2993:2998 StreamsLib <> concat def

R3002:3002 StreamsLib <> s var

R3000:3000 StreamsLib <> p var

R2990:2990 StreamsLib <> P var

R3090:3093 Coq.Lists.Streams <> Cons constr

R3090:3093 Coq.Lists.Streams <> Cons constr

def 3160:3163 <> lift

R3174:3174 StreamsLib <> A var

R3180:3183 Coq.Lists.Streams <> Cons constr

R3188:3191 StreamsLib <> lift def

R3193:3193 StreamsLib <> v var

R3185:3185 StreamsLib <> v var

prf 3204:3210 <> hd_lift

R3230:3230 StreamsLib <> A var

R3245:3247 Coq.Init.Logic <> :type_scope:x_'='_x not

R3234:3235 Coq.Lists.Streams <> hd def

R3238:3241 StreamsLib <> lift def

R3243:3243 StreamsLib <> v var

R3248:3248 StreamsLib <> v var

prf 3283:3289 <> tl_lift

R3309:3309 StreamsLib <> A var

R3324:3326 Coq.Init.Logic <> :type_scope:x_'='_x not

R3313:3314 Coq.Lists.Streams <> tl def

R3317:3320 StreamsLib <> lift def

R3322:3322 StreamsLib <> v var

R3327:3330 StreamsLib <> lift def

R3332:3332 StreamsLib <> v var

def 3372:3376 <> apply

R3387:3392 StreamsLib <> applyT def

R3403:3403 StreamsLib <> B var

R3401:3401 StreamsLib <> A var

R3394:3399 Coq.Lists.Streams <> Stream coind

R3430:3430 StreamsLib <> a var

R3427:3427 StreamsLib <> f var

R3441:3444 Coq.Lists.Streams <> Cons constr

R3455:3458 Coq.Lists.Streams <> Cons constr

R3470:3473 Coq.Lists.Streams <> Cons constr

R3484:3488 StreamsLib <> apply def

prf 3510:3517 <> hd_apply

R3539:3544 Coq.Lists.Streams <> Stream coind

R3552:3552 StreamsLib <> B var

R3547:3547 StreamsLib <> A var

R3561:3566 Coq.Lists.Streams <> Stream coind

R3568:3568 StreamsLib <> A var

R3586:3588 Coq.Init.Logic <> :type_scope:x_'='_x not

R3572:3573 Coq.Lists.Streams <> hd def

R3576:3580 StreamsLib <> apply def

R3584:3584 StreamsLib <> a var

R3582:3582 StreamsLib <> f var

R3590:3591 Coq.Lists.Streams <> hd def

R3593:3593 StreamsLib <> f var

R3597:3598 Coq.Lists.Streams <> hd def

R3600:3600 StreamsLib <> a var

prf 3660:3667 <> tl_apply

R3689:3694 Coq.Lists.Streams <> Stream coind

R3702:3702 StreamsLib <> B var

R3697:3697 StreamsLib <> A var

R3711:3716 Coq.Lists.Streams <> Stream coind

R3718:3718 StreamsLib <> A var

R3736:3738 Coq.Init.Logic <> :type_scope:x_'='_x not

R3722:3723 Coq.Lists.Streams <> tl def

R3726:3730 StreamsLib <> apply def

R3734:3734 StreamsLib <> a var

R3732:3732 StreamsLib <> f var

R3739:3743 StreamsLib <> apply def

R3753:3754 Coq.Lists.Streams <> tl def

R3756:3756 StreamsLib <> a var

R3746:3747 Coq.Lists.Streams <> tl def

R3749:3749 StreamsLib <> f var

prf 3816:3825 <> cons_apply

R3853:3853 StreamsLib <> B var

R3848:3848 StreamsLib <> A var

R3862:3867 Coq.Lists.Streams <> Stream coind

R3875:3875 StreamsLib <> B var

R3870:3870 StreamsLib <> A var

R3885:3885 StreamsLib <> A var

R3894:3899 Coq.Lists.Streams <> Stream coind

R3901:3901 StreamsLib <> A var

R3905:3908 Coq.Lists.Streams <> EqSt coind

R3945:3948 Coq.Lists.Streams <> Cons constr

R3959:3963 StreamsLib <> apply def

R3968:3969 StreamsLib <> a' var

R3965:3966 StreamsLib <> f' var

R3951:3952 StreamsLib <> f0 var

R3954:3955 StreamsLib <> a0 var

R3911:3915 StreamsLib <> apply def

R3931:3934 Coq.Lists.Streams <> Cons constr

R3939:3940 StreamsLib <> a' var

R3936:3937 StreamsLib <> a0 var

R3918:3921 Coq.Lists.Streams <> Cons constr

R3926:3927 StreamsLib <> f' var

R3923:3924 StreamsLib <> f0 var

R3995:3998 Coq.Lists.Streams <> eqst constr

R3995:3998 Coq.Lists.Streams <> eqst constr

R4023:4033 Coq.Lists.Streams <> EqSt_reflex thm

R4023:4033 Coq.Lists.Streams <> EqSt_reflex thm

prf 4048:4057 <> eqst_apply

R4082:4087 Coq.Lists.Streams <> Stream coind

R4095:4095 StreamsLib <> B var

R4090:4090 StreamsLib <> A var

R4107:4112 Coq.Lists.Streams <> Stream coind

R4114:4114 StreamsLib <> A var

R4146:4149 Coq.Lists.Streams <> EqSt coind

R4164:4168 StreamsLib <> apply def

R4173:4174 StreamsLib <> a' var

R4170:4171 StreamsLib <> f' var

R4152:4156 StreamsLib <> apply def

R4160:4160 StreamsLib <> a var

R4158:4158 StreamsLib <> f var

R4133:4136 Coq.Lists.Streams <> EqSt coind

R4140:4141 StreamsLib <> a' var

R4138:4138 StreamsLib <> a var

R4120:4123 Coq.Lists.Streams <> EqSt coind

R4127:4128 StreamsLib <> f' var

R4125:4125 StreamsLib <> f var

R4251:4254 Coq.Lists.Streams <> eqst constr

R4251:4254 Coq.Lists.Streams <> eqst constr

R4266:4273 StreamsLib <> hd_apply thm

R4266:4273 StreamsLib <> hd_apply thm

R4285:4292 StreamsLib <> hd_apply thm

R4285:4292 StreamsLib <> hd_apply thm

R4318:4325 StreamsLib <> tl_apply thm

R4318:4325 StreamsLib <> tl_apply thm

R4337:4344 StreamsLib <> tl_apply thm

R4337:4344 StreamsLib <> tl_apply thm

prf 4404:4410 <> inv_map

R4437:4437 StreamsLib <> B var

R4432:4432 StreamsLib <> A var

R4447:4452 Coq.Lists.Streams <> Stream coind

R4454:4454 StreamsLib <> A var

R4489:4494 Coq.Lists.Streams <> ForAll coind

R4530:4530 StreamsLib <> s var

R4507:4507 StreamsLib <> P var

R4510:4514 StreamsLib <> apply def

R4525:4526 StreamsLib <> s' var

R4517:4520 StreamsLib <> lift def

R4522:4522 StreamsLib <> f var

R4458:4463 Coq.Lists.Streams <> ForAll coind

R4468:4472 StreamsLib <> apply def

R4483:4483 StreamsLib <> s var

R4475:4478 StreamsLib <> lift def

R4480:4480 StreamsLib <> f var

R4465:4465 StreamsLib <> P var

R4621:4634 Coq.Lists.Streams <> HereAndFurther constr

R4621:4634 Coq.Lists.Streams <> HereAndFurther constr

prf 4700:4706 <> map_inv

R4733:4733 StreamsLib <> B var

R4728:4728 StreamsLib <> A var

R4743:4748 Coq.Lists.Streams <> Stream coind

R4750:4750 StreamsLib <> A var

R4800:4805 Coq.Lists.Streams <> ForAll coind

R4810:4814 StreamsLib <> apply def

R4825:4825 StreamsLib <> s var

R4817:4820 StreamsLib <> lift def

R4822:4822 StreamsLib <> f var

R4807:4807 StreamsLib <> P var

R4754:4759 Coq.Lists.Streams <> ForAll coind

R4795:4795 StreamsLib <> s var

R4772:4772 StreamsLib <> P var

R4775:4779 StreamsLib <> apply def

R4790:4791 StreamsLib <> s' var

R4782:4785 StreamsLib <> lift def

R4787:4787 StreamsLib <> f var

R4917:4930 Coq.Lists.Streams <> HereAndFurther constr

R4917:4930 Coq.Lists.Streams <> HereAndFurther constr

prf 4996:5002 <> evt_map

R5029:5029 StreamsLib <> B var

R5024:5024 StreamsLib <> A var

R5039:5044 Coq.Lists.Streams <> Stream coind

R5046:5046 StreamsLib <> A var

R5081:5086 Coq.Lists.Streams <> Exists ind

R5122:5122 StreamsLib <> s var

R5099:5099 StreamsLib <> P var

R5102:5106 StreamsLib <> apply def

R5117:5118 StreamsLib <> s' var

R5109:5112 StreamsLib <> lift def

R5114:5114 StreamsLib <> f var

R5050:5055 Coq.Lists.Streams <> Exists ind

R5060:5064 StreamsLib <> apply def

R5075:5075 StreamsLib <> s var

R5067:5070 StreamsLib <> lift def

R5072:5072 StreamsLib <> f var

R5057:5057 StreamsLib <> P var

R5160:5164 StreamsLib <> apply def

R5167:5170 StreamsLib <> lift def

R5160:5164 StreamsLib <> apply def

R5167:5170 StreamsLib <> lift def

R5239:5242 Coq.Lists.Streams <> Here constr

R5239:5242 Coq.Lists.Streams <> Here constr

R5291:5297 Coq.Lists.Streams <> Further constr

R5291:5297 Coq.Lists.Streams <> Further constr

R5318:5319 Coq.Lists.Streams <> tl def

R5318:5319 Coq.Lists.Streams <> tl def

R5338:5344 StreamsLib <> tl_lift thm

R5338:5344 StreamsLib <> tl_lift thm

R5359:5366 StreamsLib <> tl_apply thm

R5359:5366 StreamsLib <> tl_apply thm

R5376:5382 Coq.Init.Logic <> f_equal thm

R5376:5382 Coq.Init.Logic <> f_equal thm

prf 5413:5419 <> map_evt

R5446:5446 StreamsLib <> B var

R5441:5441 StreamsLib <> A var

R5456:5461 Coq.Lists.Streams <> Stream coind

R5463:5463 StreamsLib <> A var

R5513:5518 Coq.Lists.Streams <> Exists ind

R5523:5527 StreamsLib <> apply def

R5538:5538 StreamsLib <> s var

R5530:5533 StreamsLib <> lift def

R5535:5535 StreamsLib <> f var

R5520:5520 StreamsLib <> P var

R5467:5472 Coq.Lists.Streams <> Exists ind

R5508:5508 StreamsLib <> s var

R5485:5485 StreamsLib <> P var

R5488:5492 StreamsLib <> apply def

R5503:5504 StreamsLib <> s' var

R5495:5498 StreamsLib <> lift def

R5500:5500 StreamsLib <> f var

R5596:5599 Coq.Lists.Streams <> Here constr

R5596:5599 Coq.Lists.Streams <> Here constr

R5620:5626 Coq.Lists.Streams <> Further constr

R5620:5626 Coq.Lists.Streams <> Further constr

R5638:5645 StreamsLib <> tl_apply thm

R5638:5645 StreamsLib <> tl_apply thm

R5657:5663 StreamsLib <> tl_lift thm

R5657:5663 StreamsLib <> tl_lift thm

def 5700:5702 <> zip

R5723:5725 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R5715:5720 Coq.Lists.Streams <> Stream coind

R5722:5722 StreamsLib <> A var

R5726:5731 Coq.Lists.Streams <> Stream coind

R5733:5733 StreamsLib <> B var

R5739:5743 StreamsLib <> apply def

R5789:5791 Coq.Init.Datatypes <> snd def

R5793:5793 StreamsLib <> s var

R5746:5750 StreamsLib <> apply def

R5780:5782 Coq.Init.Datatypes <> fst def

R5784:5784 StreamsLib <> s var

R5753:5756 StreamsLib <> lift def

R5770:5770 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5772:5773 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5775:5775 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5771:5771 StreamsLib <> a var

R5774:5774 StreamsLib <> b var

prf 5804:5815 <> zip_fst_eqst

R5850:5855 Coq.Lists.Streams <> Stream coind

R5857:5857 StreamsLib <> A var

R5870:5875 Coq.Lists.Streams <> Stream coind

R5877:5877 StreamsLib <> B var

R5923:5926 Coq.Lists.Streams <> EqSt coind

R5931:5933 StreamsLib <> s1' var

R5928:5929 StreamsLib <> s1 var

R5883:5886 Coq.Lists.Streams <> EqSt coind

R5904:5906 StreamsLib <> zip def

R5908:5908 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5912:5913 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5917:5917 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5909:5911 StreamsLib <> s1' var

R5914:5916 StreamsLib <> s2' var

R5889:5891 StreamsLib <> zip def

R5893:5893 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5896:5897 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5900:5900 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R5894:5895 StreamsLib <> s1 var

R5898:5899 StreamsLib <> s2 var

R6048:6051 Coq.Lists.Streams <> eqst constr

R6048:6051 Coq.Lists.Streams <> eqst constr

prf 6167:6173 <> zip_fst

R6208:6213 Coq.Lists.Streams <> Stream coind

R6215:6215 StreamsLib <> A var

R6228:6233 Coq.Lists.Streams <> Stream coind

R6235:6235 StreamsLib <> B var

R6276:6278 Coq.Init.Logic <> :type_scope:x_'='_x not

R6274:6275 StreamsLib <> s1 var

R6279:6281 StreamsLib <> s1' var

R6253:6255 Coq.Init.Logic <> :type_scope:x_'='_x not

R6241:6243 StreamsLib <> zip def

R6245:6245 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6248:6249 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6252:6252 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6246:6247 StreamsLib <> s1 var

R6250:6251 StreamsLib <> s2 var

R6256:6258 StreamsLib <> zip def

R6260:6260 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6264:6265 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6269:6269 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6261:6263 StreamsLib <> s1' var

R6266:6268 StreamsLib <> s2' var

R6305:6311 StreamsLib <> eqst_eq prfax

R6305:6311 StreamsLib <> eqst_eq prfax

R6321:6332 StreamsLib <> zip_fst_eqst thm

R6321:6332 StreamsLib <> zip_fst_eqst thm

R6367:6377 Coq.Lists.Streams <> EqSt_reflex thm

R6367:6377 Coq.Lists.Streams <> EqSt_reflex thm

prf 6392:6403 <> zip_snd_eqst

R6438:6443 Coq.Lists.Streams <> Stream coind

R6445:6445 StreamsLib <> A var

R6458:6463 Coq.Lists.Streams <> Stream coind

R6465:6465 StreamsLib <> B var

R6511:6514 Coq.Lists.Streams <> EqSt coind

R6519:6521 StreamsLib <> s2' var

R6516:6517 StreamsLib <> s2 var

R6471:6474 Coq.Lists.Streams <> EqSt coind

R6492:6494 StreamsLib <> zip def

R6496:6496 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6500:6501 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6505:6505 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6497:6499 StreamsLib <> s1' var

R6502:6504 StreamsLib <> s2' var

R6477:6479 StreamsLib <> zip def

R6481:6481 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6484:6485 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6488:6488 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6482:6483 StreamsLib <> s1 var

R6486:6487 StreamsLib <> s2 var

R6636:6639 Coq.Lists.Streams <> eqst constr

R6636:6639 Coq.Lists.Streams <> eqst constr

prf 6755:6761 <> zip_snd

R6796:6801 Coq.Lists.Streams <> Stream coind

R6803:6803 StreamsLib <> A var

R6816:6821 Coq.Lists.Streams <> Stream coind

R6823:6823 StreamsLib <> B var

R6864:6866 Coq.Init.Logic <> :type_scope:x_'='_x not

R6862:6863 StreamsLib <> s2 var

R6867:6869 StreamsLib <> s2' var

R6841:6843 Coq.Init.Logic <> :type_scope:x_'='_x not

R6829:6831 StreamsLib <> zip def

R6833:6833 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6836:6837 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6840:6840 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6834:6835 StreamsLib <> s1 var

R6838:6839 StreamsLib <> s2 var

R6844:6846 StreamsLib <> zip def

R6848:6848 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6852:6853 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6857:6857 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R6849:6851 StreamsLib <> s1' var

R6854:6856 StreamsLib <> s2' var

R6893:6899 StreamsLib <> eqst_eq prfax

R6893:6899 StreamsLib <> eqst_eq prfax

R6909:6920 StreamsLib <> zip_snd_eqst thm

R6909:6920 StreamsLib <> zip_snd_eqst thm

R6955:6965 Coq.Lists.Streams <> EqSt_reflex thm

R6955:6965 Coq.Lists.Streams <> EqSt_reflex thm

def 6985:6989 <> unzip

R7002:7007 Coq.Lists.Streams <> Stream coind

R7011:7011 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R7010:7010 StreamsLib <> A var

R7012:7012 StreamsLib <> B var

R7019:7019 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7045:7046 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7072:7072 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7020:7024 StreamsLib <> apply def

R7044:7044 StreamsLib <> s var

R7027:7030 StreamsLib <> lift def

R7034:7036 Coq.Init.Datatypes <> fst def

R7047:7051 StreamsLib <> apply def

R7071:7071 StreamsLib <> s var

R7054:7057 StreamsLib <> lift def

R7061:7063 Coq.Init.Datatypes <> snd def

prf 7082:7093 <> fst_zip_eqst

R7116:7121 Coq.Lists.Streams <> Stream coind

R7123:7123 StreamsLib <> A var

R7132:7137 Coq.Lists.Streams <> Stream coind

R7139:7139 StreamsLib <> B var

R7143:7146 Coq.Lists.Streams <> EqSt coind

R7189:7190 StreamsLib <> s1 var

R7149:7153 StreamsLib <> apply def

R7174:7176 StreamsLib <> zip def

R7178:7178 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7181:7182 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7185:7185 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7179:7180 StreamsLib <> s1 var

R7183:7184 StreamsLib <> s2 var

R7156:7159 StreamsLib <> lift def

R7163:7165 Coq.Init.Datatypes <> fst def

R7257:7260 Coq.Lists.Streams <> eqst constr

R7257:7260 Coq.Lists.Streams <> eqst constr

prf 7304:7310 <> fst_zip

R7333:7338 Coq.Lists.Streams <> Stream coind

R7340:7340 StreamsLib <> A var

R7349:7354 Coq.Lists.Streams <> Stream coind

R7356:7356 StreamsLib <> B var

R7398:7400 Coq.Init.Logic <> :type_scope:x_'='_x not

R7360:7364 StreamsLib <> apply def

R7385:7387 StreamsLib <> zip def

R7389:7389 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7392:7393 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7396:7396 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7390:7391 StreamsLib <> s1 var

R7394:7395 StreamsLib <> s2 var

R7367:7370 StreamsLib <> lift def

R7374:7376 Coq.Init.Datatypes <> fst def

R7401:7402 StreamsLib <> s1 var

R7426:7432 StreamsLib <> eqst_eq prfax

R7426:7432 StreamsLib <> eqst_eq prfax

R7441:7452 StreamsLib <> fst_zip_eqst thm

R7441:7452 StreamsLib <> fst_zip_eqst thm

prf 7467:7478 <> snd_zip_eqst

R7501:7506 Coq.Lists.Streams <> Stream coind

R7508:7508 StreamsLib <> A var

R7517:7522 Coq.Lists.Streams <> Stream coind

R7524:7524 StreamsLib <> B var

R7528:7531 Coq.Lists.Streams <> EqSt coind

R7574:7575 StreamsLib <> s2 var

R7534:7538 StreamsLib <> apply def

R7559:7561 StreamsLib <> zip def

R7563:7563 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7566:7567 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7570:7570 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7564:7565 StreamsLib <> s1 var

R7568:7569 StreamsLib <> s2 var

R7541:7544 StreamsLib <> lift def

R7548:7550 Coq.Init.Datatypes <> snd def

R7642:7645 Coq.Lists.Streams <> eqst constr

R7642:7645 Coq.Lists.Streams <> eqst constr

prf 7689:7695 <> snd_zip

R7718:7723 Coq.Lists.Streams <> Stream coind

R7725:7725 StreamsLib <> A var

R7734:7739 Coq.Lists.Streams <> Stream coind

R7741:7741 StreamsLib <> B var

R7783:7785 Coq.Init.Logic <> :type_scope:x_'='_x not

R7745:7749 StreamsLib <> apply def

R7770:7772 StreamsLib <> zip def

R7774:7774 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7777:7778 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7781:7781 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R7775:7776 StreamsLib <> s1 var

R7779:7780 StreamsLib <> s2 var

R7752:7755 StreamsLib <> lift def

R7759:7761 Coq.Init.Datatypes <> snd def

R7786:7787 StreamsLib <> s2 var

R7811:7817 StreamsLib <> eqst_eq prfax

R7811:7817 StreamsLib <> eqst_eq prfax

R7826:7837 StreamsLib <> snd_zip_eqst thm

R7826:7837 StreamsLib <> snd_zip_eqst thm

prf 7852:7865 <> zip_unzip_eqst

R7887:7892 Coq.Lists.Streams <> Stream coind

R7896:7896 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R7895:7895 StreamsLib <> A var

R7897:7897 StreamsLib <> B var

R7902:7905 Coq.Lists.Streams <> EqSt coind

R7923:7923 StreamsLib <> s var

R7908:7910 StreamsLib <> zip def

R7913:7917 StreamsLib <> unzip def

R7919:7919 StreamsLib <> s var

R7976:7979 Coq.Lists.Streams <> eqst constr

R7976:7979 Coq.Lists.Streams <> eqst constr

prf 8052:8060 <> zip_unzip

R8082:8087 Coq.Lists.Streams <> Stream coind

R8091:8091 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R8090:8090 StreamsLib <> A var

R8092:8092 StreamsLib <> B var

R8110:8112 Coq.Init.Logic <> :type_scope:x_'='_x not

R8097:8099 StreamsLib <> zip def

R8102:8106 StreamsLib <> unzip def

R8108:8108 StreamsLib <> s var

R8113:8113 StreamsLib <> s var

R8137:8143 StreamsLib <> eqst_eq prfax

R8137:8143 StreamsLib <> eqst_eq prfax

R8152:8165 StreamsLib <> zip_unzip_eqst thm

R8152:8165 StreamsLib <> zip_unzip_eqst thm

prf 8182:8192 <> inv_eq_eqst

R8215:8220 Coq.Lists.Streams <> Stream coind

R8222:8222 StreamsLib <> A var

R8292:8295 Coq.Lists.Streams <> EqSt coind

R8299:8300 StreamsLib <> s' var

R8297:8297 StreamsLib <> s var

R8227:8232 Coq.Lists.Streams <> ForAll coind

R8276:8278 StreamsLib <> zip def

R8280:8280 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8282:8283 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8286:8286 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8281:8281 StreamsLib <> s var

R8284:8285 StreamsLib <> s' var

R8258:8260 Coq.Init.Logic <> :type_scope:x_'='_x not

R8246:8248 Coq.Init.Datatypes <> fst def

R8251:8252 Coq.Lists.Streams <> hd def

R8254:8256 StreamsLib <> ss' var

R8261:8263 Coq.Init.Datatypes <> snd def

R8266:8267 Coq.Lists.Streams <> hd def

R8269:8271 StreamsLib <> ss' var

R8408:8411 Coq.Lists.Streams <> eqst constr

R8408:8411 Coq.Lists.Streams <> eqst constr

prf 8469:8479 <> eqst_inv_eq

R8502:8507 Coq.Lists.Streams <> Stream coind

R8509:8509 StreamsLib <> A var

R8528:8533 Coq.Lists.Streams <> ForAll coind

R8577:8579 StreamsLib <> zip def

R8581:8581 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8583:8584 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8587:8587 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8582:8582 StreamsLib <> s var

R8585:8586 StreamsLib <> s' var

R8559:8561 Coq.Init.Logic <> :type_scope:x_'='_x not

R8547:8549 Coq.Init.Datatypes <> fst def

R8552:8553 Coq.Lists.Streams <> hd def

R8555:8557 StreamsLib <> ss' var

R8562:8564 Coq.Init.Datatypes <> snd def

R8567:8568 Coq.Lists.Streams <> hd def

R8570:8572 StreamsLib <> ss' var

R8515:8518 Coq.Lists.Streams <> EqSt coind

R8522:8523 StreamsLib <> s' var

R8520:8520 StreamsLib <> s var

R8696:8709 Coq.Lists.Streams <> HereAndFurther constr

R8696:8709 Coq.Lists.Streams <> HereAndFurther constr

def 8771:8781 <> history_rec

R8795:8798 Coq.Init.Datatypes <> list ind

R8800:8800 StreamsLib <> A var

R8808:8813 Coq.Lists.Streams <> Stream coind

R8815:8815 StreamsLib <> A var

R8820:8825 Coq.Lists.Streams <> Stream coind

R8834:8836 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R8828:8831 Coq.Init.Datatypes <> list ind

R8833:8833 StreamsLib <> A var

R8837:8837 StreamsLib <> A var

R8850:8850 StreamsLib <> s var

R8860:8863 Coq.Lists.Streams <> Cons constr

R8874:8877 Coq.Lists.Streams <> Cons constr

R8891:8901 StreamsLib <> history_rec def

R8904:8907 Coq.Init.Datatypes <> cons constr

R8912:8915 StreamsLib <> past var

R8879:8879 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8884:8885 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8888:8888 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not

R8880:8883 StreamsLib <> past var

def 8940:8946 <> history

R8957:8962 Coq.Lists.Streams <> Stream coind

R8964:8964 StreamsLib <> A var

R8969:8974 Coq.Lists.Streams <> Stream coind

R8983:8985 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R8977:8980 Coq.Init.Datatypes <> list ind

R8982:8982 StreamsLib <> A var

R8986:8986 StreamsLib <> A var

R8992:9002 StreamsLib <> history_rec def

R9008:9008 StreamsLib <> s var

R9004:9006 Coq.Init.Datatypes <> nil constr

prf 9021:9036 <> eqst_history_rec

R9058:9061 Coq.Init.Datatypes <> list ind

R9063:9063 StreamsLib <> A var

R9078:9083 Coq.Lists.Streams <> Stream coind

R9085:9085 StreamsLib <> A var

R9108:9111 Coq.Lists.Streams <> EqSt coind

R9136:9146 StreamsLib <> history_rec def

R9152:9155 StreamsLib <> sfx' var

R9148:9150 StreamsLib <> pfx var

R9114:9124 StreamsLib <> history_rec def

R9130:9132 StreamsLib <> sfx var

R9126:9128 StreamsLib <> pfx var

R9091:9094 Coq.Lists.Streams <> EqSt coind

R9100:9103 StreamsLib <> sfx' var

R9096:9098 StreamsLib <> sfx var

R9305:9308 Coq.Lists.Streams <> eqst constr

R9305:9308 Coq.Lists.Streams <> eqst constr

prf 9382:9393 <> eqst_history

R9420:9425 Coq.Lists.Streams <> Stream coind

R9427:9427 StreamsLib <> A var

R9450:9453 Coq.Lists.Streams <> EqSt coind

R9470:9476 StreamsLib <> history def

R9478:9481 StreamsLib <> sfx' var

R9456:9462 StreamsLib <> history def

R9464:9466 StreamsLib <> sfx var

R9433:9436 Coq.Lists.Streams <> EqSt coind

R9442:9445 StreamsLib <> sfx' var

R9438:9440 StreamsLib <> sfx var

R9506:9521 StreamsLib <> eqst_history_rec thm

R9506:9521 StreamsLib <> eqst_history_rec thm

prf 9550:9566 <> unzip_history_rec

R9588:9591 Coq.Init.Datatypes <> list ind

R9593:9593 StreamsLib <> A var

R9603:9608 Coq.Lists.Streams <> Stream coind

R9610:9610 StreamsLib <> A var

R9614:9617 Coq.Lists.Streams <> EqSt coind

R9655:9657 StreamsLib <> sfx var

R9620:9622 Coq.Init.Datatypes <> snd def

R9625:9629 StreamsLib <> unzip def

R9632:9642 StreamsLib <> history_rec def

R9648:9650 StreamsLib <> sfx var

R9644:9646 StreamsLib <> pfx var

R9725:9728 Coq.Lists.Streams <> eqst constr

R9725:9728 Coq.Lists.Streams <> eqst constr

prf 9774:9786 <> unzip_history

R9806:9811 Coq.Lists.Streams <> Stream coind

R9813:9813 StreamsLib <> A var

R9817:9820 Coq.Lists.Streams <> EqSt coind

R9848:9848 StreamsLib <> s var

R9823:9825 Coq.Init.Datatypes <> snd def

R9828:9832 StreamsLib <> unzip def

R9835:9841 StreamsLib <> history def

R9843:9843 StreamsLib <> s var

R9865:9871 StreamsLib <> history def

R9888:9904 StreamsLib <> unzip_history_rec thm

R9888:9904 StreamsLib <> unzip_history_rec thm

def 9924:9935 <> History_Spec

R9946:9951 Coq.Lists.Streams <> Stream coind

R9953:9953 StreamsLib <> A var

R10018:10023 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R9983:9985 Coq.Init.Logic <> :type_scope:x_'='_x not

R9967:9969 Coq.Init.Datatypes <> fst def

R9972:9973 Coq.Lists.Streams <> hd def

R9976:9977 Coq.Lists.Streams <> tl def

R9979:9980 StreamsLib <> s' var

R9986:9989 Coq.Init.Datatypes <> cons constr

R10006:10008 Coq.Init.Datatypes <> fst def

R10011:10012 Coq.Lists.Streams <> hd def

R10014:10015 StreamsLib <> s' var

R9992:9994 Coq.Init.Datatypes <> snd def

R9997:9998 Coq.Lists.Streams <> hd def

R10000:10001 StreamsLib <> s' var

R10024:10027 Coq.Lists.Streams <> EqSt coind

R10081:10081 StreamsLib <> s var

R10030:10035 StreamsLib <> concat def

R10052:10056 StreamsLib <> apply def

R10076:10077 StreamsLib <> s' var

R10059:10062 StreamsLib <> lift def

R10066:10068 Coq.Init.Datatypes <> snd def

R10038:10040 Coq.Init.Datatypes <> fst def

R10043:10044 Coq.Lists.Streams <> hd def

R10046:10047 StreamsLib <> s' var

prf 10093:10108 <> history_rec_spec

R10130:10135 Coq.Lists.Streams <> Stream coind

R10137:10137 StreamsLib <> A var

R10176:10182 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R10172:10174 Coq.Init.Logic <> :type_scope:x_'='_x not

R10146:10148 Coq.Init.Datatypes <> fst def

R10151:10152 Coq.Lists.Streams <> hd def

R10155:10165 StreamsLib <> history_rec def

R10169:10169 StreamsLib <> s var

R10167:10167 StreamsLib <> p var

R10175:10175 StreamsLib <> p var

R10183:10188 Coq.Lists.Streams <> ForAll coind

R10232:10242 StreamsLib <> history_rec def

R10246:10246 StreamsLib <> s var

R10244:10244 StreamsLib <> p var

R10201:10212 StreamsLib <> History_Spec def

R10227:10228 StreamsLib <> s' var

R10215:10220 StreamsLib <> concat def

R10224:10224 StreamsLib <> s var

R10222:10222 StreamsLib <> p var

R10359:10372 Coq.Lists.Streams <> HereAndFurther constr

R10359:10372 Coq.Lists.Streams <> HereAndFurther constr

R10436:10446 StreamsLib <> eqst_concat thm

R10436:10446 StreamsLib <> eqst_concat thm

R10458:10474 StreamsLib <> unzip_history_rec thm

R10458:10474 StreamsLib <> unzip_history_rec thm

R10494:10497 Coq.Init.Datatypes <> cons constr

R10494:10497 Coq.Init.Datatypes <> cons constr

prf 10524:10535 <> history_spec

R10555:10560 Coq.Lists.Streams <> Stream coind

R10562:10562 StreamsLib <> A var

R10597:10602 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R10591:10593 Coq.Init.Logic <> :type_scope:x_'='_x not

R10571:10573 Coq.Init.Datatypes <> fst def

R10576:10577 Coq.Lists.Streams <> hd def

R10580:10586 StreamsLib <> history def

R10588:10588 StreamsLib <> s var

R10594:10596 Coq.Init.Datatypes <> nil constr

R10603:10608 Coq.Lists.Streams <> ForAll coind

R10641:10647 StreamsLib <> history def

R10649:10649 StreamsLib <> s var

R10621:10632 StreamsLib <> History_Spec def

R10636:10637 StreamsLib <> s' var

R10634:10634 StreamsLib <> s var

R10680:10695 StreamsLib <> history_rec_spec thm

R10697:10699 Coq.Init.Datatypes <> nil constr

R10680:10695 StreamsLib <> history_rec_spec thm

R10697:10699 Coq.Init.Datatypes <> nil constr

R0:-1 StreamsLib <> y var

prf 10730:10754 <> history_rec_spec_complete

R10776:10781 Coq.Lists.Streams <> Stream coind

R10783:10783 StreamsLib <> A var

R10865:10868 Coq.Lists.Streams <> EqSt coind

R10874:10884 StreamsLib <> history_rec def

R10888:10888 StreamsLib <> s var

R10886:10886 StreamsLib <> p var

R10870:10871 StreamsLib <> ps var

R10811:10816 Coq.Lists.Streams <> ForAll coind

R10859:10860 StreamsLib <> ps var

R10829:10840 StreamsLib <> History_Spec def

R10855:10856 StreamsLib <> s' var

R10843:10848 StreamsLib <> concat def

R10852:10852 StreamsLib <> s var

R10850:10850 StreamsLib <> p var

R10803:10805 Coq.Init.Logic <> :type_scope:x_'='_x not

R10792:10794 Coq.Init.Datatypes <> fst def

R10797:10798 Coq.Lists.Streams <> hd def

R10800:10801 StreamsLib <> ps var

R10806:10806 StreamsLib <> p var

R11031:11042 StreamsLib <> History_Spec def

R11080:11083 Coq.Lists.Streams <> eqst constr

R11080:11083 Coq.Lists.Streams <> eqst constr

R11147:11158 StreamsLib <> History_Spec def

R11212:11222 StreamsLib <> concat_eqst thm

R11232:11241 Coq.Init.Logic <> refl_equal syndef

R11212:11222 StreamsLib <> concat_eqst thm

R11232:11241 Coq.Init.Logic <> refl_equal syndef

R11349:11359 StreamsLib <> concat_eqst thm

R11369:11378 Coq.Init.Logic <> refl_equal syndef

R11349:11359 StreamsLib <> concat_eqst thm

R11369:11378 Coq.Init.Logic <> refl_equal syndef

prf 11468:11488 <> history_spec_complete

R11508:11513 Coq.Lists.Streams <> Stream coind

R11515:11515 StreamsLib <> A var

R11588:11591 Coq.Lists.Streams <> EqSt coind

R11597:11603 StreamsLib <> history def

R11605:11605 StreamsLib <> s var

R11593:11594 StreamsLib <> ps var

R11545:11550 Coq.Lists.Streams <> ForAll coind

R11582:11583 StreamsLib <> ps var

R11563:11574 StreamsLib <> History_Spec def

R11578:11579 StreamsLib <> s' var

R11576:11576 StreamsLib <> s var

R11535:11537 Coq.Init.Logic <> :type_scope:x_'='_x not

R11524:11526 Coq.Init.Datatypes <> fst def

R11529:11530 Coq.Lists.Streams <> hd def

R11532:11533 StreamsLib <> ps var

R11538:11540 Coq.Init.Datatypes <> nil constr

R11630:11654 StreamsLib <> history_rec_spec_complete thm

R11630:11654 StreamsLib <> history_rec_spec_complete thm

prf 11698:11722 <> inv_snd_history_rec_intro

R11742:11747 Coq.Lists.Streams <> Stream coind

R11749:11749 StreamsLib <> A var

R11767:11772 Coq.Lists.Streams <> Stream coind

R11774:11774 StreamsLib <> A var

R11794:11799 Coq.Lists.Streams <> ForAll coind

R11845:11855 StreamsLib <> history_rec def

R11859:11859 StreamsLib <> s var

R11857:11857 StreamsLib <> p var

R11812:11812 StreamsLib <> P var

R11815:11819 StreamsLib <> apply def

R11839:11840 StreamsLib <> s' var

R11822:11825 StreamsLib <> lift def

R11829:11831 Coq.Init.Datatypes <> snd def

R11780:11785 Coq.Lists.Streams <> ForAll coind

R11789:11789 StreamsLib <> s var

R11787:11787 StreamsLib <> P var

R11884:11890 StreamsLib <> inv_map thm

R11884:11890 StreamsLib <> inv_map thm

R11905:11911 StreamsLib <> eqst_eq prfax

R11918:11934 StreamsLib <> unzip_history_rec thm

R11905:11911 StreamsLib <> eqst_eq prfax

R11918:11934 StreamsLib <> unzip_history_rec thm

prf 11995:12015 <> inv_snd_history_intro

R12035:12040 Coq.Lists.Streams <> Stream coind

R12042:12042 StreamsLib <> A var

R12058:12063 Coq.Lists.Streams <> Stream coind

R12065:12065 StreamsLib <> A var

R12085:12090 Coq.Lists.Streams <> ForAll coind

R12136:12142 StreamsLib <> history def

R12144:12144 StreamsLib <> s var

R12103:12103 StreamsLib <> P var

R12106:12110 StreamsLib <> apply def

R12130:12131 StreamsLib <> s' var

R12113:12116 StreamsLib <> lift def

R12120:12122 Coq.Init.Datatypes <> snd def

R12071:12076 Coq.Lists.Streams <> ForAll coind

R12080:12080 StreamsLib <> s var

R12078:12078 StreamsLib <> P var

R12169:12193 StreamsLib <> inv_snd_history_rec_intro thm

R12169:12193 StreamsLib <> inv_snd_history_rec_intro thm

prf 12222:12245 <> inv_snd_history_rec_elim

R12265:12270 Coq.Lists.Streams <> Stream coind

R12272:12272 StreamsLib <> A var

R12290:12295 Coq.Lists.Streams <> Stream coind

R12297:12297 StreamsLib <> A var

R12374:12379 Coq.Lists.Streams <> ForAll coind

R12383:12383 StreamsLib <> s var

R12381:12381 StreamsLib <> P var

R12303:12308 Coq.Lists.Streams <> ForAll coind

R12354:12364 StreamsLib <> history_rec def

R12368:12368 StreamsLib <> s var

R12366:12366 StreamsLib <> p var

R12321:12321 StreamsLib <> P var

R12324:12328 StreamsLib <> apply def

R12348:12349 StreamsLib <> s' var

R12331:12334 StreamsLib <> lift def

R12338:12340 Coq.Init.Datatypes <> snd def

R12413:12419 StreamsLib <> eqst_eq prfax

R12426:12442 StreamsLib <> unzip_history_rec thm

R12413:12419 StreamsLib <> eqst_eq prfax

R12426:12442 StreamsLib <> unzip_history_rec thm

R12457:12463 StreamsLib <> map_inv thm

R12457:12463 StreamsLib <> map_inv thm

prf 12489:12508 <> inv_snd_history_elim

R12528:12533 Coq.Lists.Streams <> Stream coind

R12535:12535 StreamsLib <> A var

R12551:12556 Coq.Lists.Streams <> Stream coind

R12558:12558 StreamsLib <> A var

R12629:12634 Coq.Lists.Streams <> ForAll coind

R12638:12638 StreamsLib <> s var

R12636:12636 StreamsLib <> P var

R12564:12569 Coq.Lists.Streams <> ForAll coind

R12615:12621 StreamsLib <> history def

R12623:12623 StreamsLib <> s var

R12582:12582 StreamsLib <> P var

R12585:12589 StreamsLib <> apply def

R12609:12610 StreamsLib <> s' var

R12592:12595 StreamsLib <> lift def

R12599:12601 Coq.Init.Datatypes <> snd def

R12698:12700 Coq.Init.Datatypes <> nil constr

R12662:12685 StreamsLib <> inv_snd_history_rec_elim thm

R12698:12700 Coq.Init.Datatypes <> nil constr

R12662:12685 StreamsLib <> inv_snd_history_rec_elim thm

def 12731:12736 <> prefix

R12747:12747 StreamsLib <> A var

R12768:12768 StreamsLib <> A var

R12763:12763 StreamsLib <> A var

R12784:12786 Coq.Init.Datatypes <> nat ind

R12791:12794 Coq.Init.Datatypes <> list ind

R12796:12796 StreamsLib <> A var

R12817:12817 StreamsLib <> k var

R12849:12852 Coq.Init.Logic <> True ind

R12858:12858 Coq.Init.Datatypes <> S constr

R12884:12884 StreamsLib <> p var

R12916:12919 Coq.Init.Logic <> True ind

R12986:12986 StreamsLib <> I var

R13016:13016 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R13023:13028 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R13044:13044 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R13017:13017 StreamsLib <> T var

R13029:13034 StreamsLib <> prefix def

R13038:13038 StreamsLib <> T var

R13036:13036 StreamsLib <> I var

prf 13077:13089 <> prefix_mono_k

R13115:13118 Coq.Init.Datatypes <> list ind

R13120:13120 StreamsLib <> A var

R13146:13151 StreamsLib <> prefix def

R13159:13159 StreamsLib <> p var

R13157:13157 StreamsLib <> k var

R13155:13155 StreamsLib <> T var

R13153:13153 StreamsLib <> I var

R13124:13129 StreamsLib <> prefix def

R13141:13141 StreamsLib <> p var

R13136:13136 Coq.Init.Datatypes <> S constr

R13138:13138 StreamsLib <> k var

R13133:13133 StreamsLib <> T var

R13131:13131 StreamsLib <> I var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

prf 13316:13327 <> prefix_apply

R13350:13350 StreamsLib <> A var

R13374:13374 StreamsLib <> A var

R13369:13369 StreamsLib <> A var

R13392:13395 Coq.Init.Datatypes <> list ind

R13397:13397 StreamsLib <> A var

R13490:13495 StreamsLib <> prefix def

R13505:13505 StreamsLib <> p var

R13503:13503 StreamsLib <> k var

R13500:13501 StreamsLib <> T' var

R13497:13498 StreamsLib <> I' var

R13421:13426 StreamsLib <> prefix def

R13485:13485 StreamsLib <> p var

R13483:13483 StreamsLib <> k var

R13474:13475 StreamsLib <> T' var

R13479:13480 StreamsLib <> s' var

R13477:13477 StreamsLib <> s var

R13464:13464 StreamsLib <> T var

R13468:13469 StreamsLib <> s' var

R13466:13466 StreamsLib <> s var

R13445:13446 StreamsLib <> I' var

R13448:13448 StreamsLib <> s var

R13438:13438 StreamsLib <> I var

R13440:13440 StreamsLib <> s var

R13403:13408 StreamsLib <> prefix def

R13416:13416 StreamsLib <> p var

R13414:13414 StreamsLib <> k var

R13412:13412 StreamsLib <> T var

R13410:13410 StreamsLib <> I var

R0:-1 StreamsLib <> y var

R0:-1 StreamsLib <> y var

prf 13649:13658 <> kinduction

R13678:13678 StreamsLib <> A var

R13696:13701 Coq.Lists.Streams <> Stream coind

R13703:13703 StreamsLib <> A var

R13827:13832 Coq.Lists.Streams <> ForAll coind

R13856:13856 StreamsLib <> s var

R13845:13845 StreamsLib <> P var

R13848:13849 Coq.Lists.Streams <> hd def

R13851:13852 StreamsLib <> s' var

R13711:13716 Coq.Lists.Streams <> ForAll coind

R13812:13818 StreamsLib <> history def

R13820:13820 StreamsLib <> s var

R13794:13794 StreamsLib <> P var

R13797:13799 Coq.Init.Datatypes <> snd def

R13802:13803 Coq.Lists.Streams <> hd def

R13805:13806 StreamsLib <> s' var

R13729:13734 StreamsLib <> prefix def

R13778:13780 Coq.Init.Datatypes <> fst def

R13783:13784 Coq.Lists.Streams <> hd def

R13786:13787 StreamsLib <> s' var

R13775:13775 StreamsLib <> k var

R13768:13768 StreamsLib <> P var

R13770:13772 StreamsLib <> st' var

R13747:13747 StreamsLib <> P var

R13749:13750 StreamsLib <> st var

R13880:13899 StreamsLib <> inv_snd_history_elim thm

R13880:13899 StreamsLib <> inv_snd_history_elim thm

R13946:13948 Coq.Init.Datatypes <> snd def

R13951:13952 Coq.Lists.Streams <> hd def

R13954:13955 StreamsLib <> s' var

R13909:13920 StreamsLib <> ForAll_apply def

R13946:13948 Coq.Init.Datatypes <> snd def

R13951:13952 Coq.Lists.Streams <> hd def

R13954:13955 StreamsLib <> s' var

R13909:13920 StreamsLib <> ForAll_apply def

R14024:14029 StreamsLib <> prefix def

R14073:14075 Coq.Init.Datatypes <> fst def

R14078:14079 Coq.Lists.Streams <> hd def

R14081:14082 StreamsLib <> s' var

R14065:14067 StreamsLib <> st' var

R14044:14045 StreamsLib <> st var

R13971:13982 StreamsLib <> ForAll_apply def

R14024:14029 StreamsLib <> prefix def

R14073:14075 Coq.Init.Datatypes <> fst def

R14078:14079 Coq.Lists.Streams <> hd def

R14081:14082 StreamsLib <> s' var

R14065:14067 StreamsLib <> st' var

R14044:14045 StreamsLib <> st var

R13971:13982 StreamsLib <> ForAll_apply def

R14138:14143 Coq.Lists.Streams <> ForAll coind

R14169:14174 Coq.Lists.Streams <> Stream coind

R14183:14185 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R14177:14180 Coq.Init.Datatypes <> list ind

R14299:14301 Coq.Init.Datatypes <> snd def

R14304:14305 Coq.Lists.Streams <> hd def

R14307:14308 StreamsLib <> s' var

R14207:14212 StreamsLib <> prefix def

R14280:14282 Coq.Init.Datatypes <> fst def

R14285:14286 Coq.Lists.Streams <> hd def

R14288:14289 StreamsLib <> s' var

R14255:14257 StreamsLib <> st' var

R14231:14232 StreamsLib <> st var

R14100:14115 StreamsLib <> ForAll_reinforce def

R14138:14143 Coq.Lists.Streams <> ForAll coind

R14169:14174 Coq.Lists.Streams <> Stream coind

R14183:14185 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R14177:14180 Coq.Init.Datatypes <> list ind

R14299:14301 Coq.Init.Datatypes <> snd def

R14304:14305 Coq.Lists.Streams <> hd def

R14307:14308 StreamsLib <> s' var

R14207:14212 StreamsLib <> prefix def

R14280:14282 Coq.Init.Datatypes <> fst def

R14285:14286 Coq.Lists.Streams <> hd def

R14288:14289 StreamsLib <> s' var

R14255:14257 StreamsLib <> st' var

R14231:14232 StreamsLib <> st var

R14100:14115 StreamsLib <> ForAll_reinforce def

R14359:14364 Coq.Lists.Streams <> ForAll coind

R14376:14381 Coq.Lists.Streams <> Stream coind

R14390:14392 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R14384:14387 Coq.Init.Datatypes <> list ind

R14399:14410 StreamsLib <> History_Spec def

R14414:14415 StreamsLib <> s' var

R14327:14342 StreamsLib <> ForAll_reinforce def

R14359:14364 Coq.Lists.Streams <> ForAll coind

R14376:14381 Coq.Lists.Streams <> Stream coind

R14390:14392 Coq.Init.Datatypes <> :type_scope:x_'*'_x not

R14384:14387 Coq.Init.Datatypes <> list ind

R14399:14410 StreamsLib <> History_Spec def

R14414:14415 StreamsLib <> s' var

R14327:14342 StreamsLib <> ForAll_reinforce def

R14429:14440 Coq.Lists.Streams <> ForAll_coind thm

R14429:14440 Coq.Lists.Streams <> ForAll_coind thm

R14472:14472 StreamsLib <> x var

R14472:14472 StreamsLib <> x var

R0:-1 StreamsLib <> y var

R14646:14657 StreamsLib <> History_Spec def

R0:-1 StreamsLib <> y var

R14925:14937 StreamsLib <> prefix_mono_k thm

R14925:14937 StreamsLib <> prefix_mono_k thm

R0:-1 StreamsLib <> y var

R14998:15009 StreamsLib <> history_spec thm

R14998:15009 StreamsLib <> history_spec thm

R0:-1 StreamsLib <> y var

R15147:15159 StreamsLib <> necessitation def

R15147:15159 StreamsLib <> necessitation def

prf 15208:15218 <> kinduction'

R15239:15239 StreamsLib <> A var

R15260:15265 Coq.Lists.Streams <> Stream coind

R15267:15267 StreamsLib <> A var

R15448:15453 Coq.Lists.Streams <> ForAll coind

R15477:15477 StreamsLib <> s var

R15466:15466 StreamsLib <> P var

R15469:15470 Coq.Lists.Streams <> hd def

R15472:15473 StreamsLib <> s' var

R15341:15346 Coq.Lists.Streams <> ForAll coind

R15441:15442 StreamsLib <> ps var

R15424:15424 StreamsLib <> P var

R15427:15429 Coq.Init.Datatypes <> snd def

R15432:15433 Coq.Lists.Streams <> hd def

R15435:15436 StreamsLib <> s' var

R15359:15364 StreamsLib <> prefix def

R15408:15410 Coq.Init.Datatypes <> fst def

R15413:15414 Coq.Lists.Streams <> hd def

R15416:15417 StreamsLib <> s' var

R15405:15405 StreamsLib <> k var

R15398:15398 StreamsLib <> P var

R15400:15402 StreamsLib <> st' var

R15377:15377 StreamsLib <> P var

R15379:15380 StreamsLib <> st var

R15297:15302 Coq.Lists.Streams <> ForAll coind

R15334:15335 StreamsLib <> ps var

R15315:15326 StreamsLib <> History_Spec def

R15330:15331 StreamsLib <> s' var

R15328:15328 StreamsLib <> s var

R15286:15288 Coq.Init.Logic <> :type_scope:x_'='_x not

R15275:15277 Coq.Init.Datatypes <> fst def

R15280:15281 Coq.Lists.Streams <> hd def

R15283:15284 StreamsLib <> ps var

R15289:15291 Coq.Init.Datatypes <> nil constr

R15504:15510 StreamsLib <> eqst_eq prfax

R15517:15537 StreamsLib <> history_spec_complete thm

R15504:15510 StreamsLib <> eqst_eq prfax

R15517:15537 StreamsLib <> history_spec_complete thm

R15564:15573 StreamsLib <> kinduction thm

R15564:15573 StreamsLib <> kinduction thm

prf 15600:15621 <> inv_prefix_history_rec

R15641:15641 StreamsLib <> A var

R15662:15662 StreamsLib <> A var

R15657:15657 StreamsLib <> A var

R15680:15685 Coq.Lists.Streams <> Stream coind

R15687:15687 StreamsLib <> A var

R15799:15804 Coq.Lists.Streams <> ForAll coind

R15867:15877 StreamsLib <> history_rec def

R15881:15881 StreamsLib <> s var

R15879:15879 StreamsLib <> p var

R15817:15822 StreamsLib <> prefix def

R15831:15834 Coq.Init.Datatypes <> cons constr

R15851:15853 Coq.Init.Datatypes <> fst def

R15856:15857 Coq.Lists.Streams <> hd def

R15859:15860 StreamsLib <> s' var

R15837:15839 Coq.Init.Datatypes <> snd def

R15842:15843 Coq.Lists.Streams <> hd def

R15845:15846 StreamsLib <> s' var

R15828:15828 StreamsLib <> k var

R15826:15826 StreamsLib <> T var

R15824:15824 StreamsLib <> I var

R15764:15769 StreamsLib <> prefix def

R15778:15781 Coq.Init.Datatypes <> cons constr

R15790:15790 StreamsLib <> p var

R15784:15785 Coq.Lists.Streams <> hd def

R15787:15787 StreamsLib <> s var

R15775:15775 StreamsLib <> k var

R15773:15773 StreamsLib <> T var

R15771:15771 StreamsLib <> I var

R15692:15697 Coq.Lists.Streams <> ForAll coind

R15735:15740 StreamsLib <> concat def

R15744:15744 StreamsLib <> s var

R15742:15742 StreamsLib <> p var

R15710:15710 StreamsLib <> T var

R15721:15722 Coq.Lists.Streams <> hd def

R15725:15726 Coq.Lists.Streams <> tl def

R15728:15729 StreamsLib <> s' var

R15713:15714 Coq.Lists.Streams <> hd def

R15716:15717 StreamsLib <> s' var

R15970:15983 Coq.Lists.Streams <> HereAndFurther constr

R15970:15983 Coq.Lists.Streams <> HereAndFurther constr

R16097:16106 StreamsLib <> inv_concat thm

R16097:16106 StreamsLib <> inv_concat thm

R16184:16196 StreamsLib <> prefix_mono_k thm

R16184:16196 StreamsLib <> prefix_mono_k thm

prf 16229:16246 <> inv_prefix_history

R16266:16266 StreamsLib <> A var

R16287:16287 StreamsLib <> A var

R16282:16282 StreamsLib <> A var

R16303:16308 Coq.Lists.Streams <> Stream coind

R16310:16310 StreamsLib <> A var

R16386:16391 Coq.Lists.Streams <> ForAll coind

R16454:16460 StreamsLib <> history def

R16462:16462 StreamsLib <> s var

R16404:16409 StreamsLib <> prefix def

R16418:16421 Coq.Init.Datatypes <> cons constr

R16438:16440 Coq.Init.Datatypes <> fst def

R16443:16444 Coq.Lists.Streams <> hd def

R16446:16447 StreamsLib <> s' var

R16424:16426 Coq.Init.Datatypes <> snd def

R16429:16430 Coq.Lists.Streams <> hd def

R16432:16433 StreamsLib <> s' var

R16415:16415 StreamsLib <> k var

R16413:16413 StreamsLib <> T var

R16411:16411 StreamsLib <> I var

R16327:16332 Coq.Lists.Streams <> ForAll coind

R16369:16369 StreamsLib <> s var

R16345:16345 StreamsLib <> T var

R16356:16357 Coq.Lists.Streams <> hd def

R16360:16361 Coq.Lists.Streams <> tl def

R16363:16364 StreamsLib <> s' var

R16348:16349 Coq.Lists.Streams <> hd def

R16351:16352 StreamsLib <> s' var

R16315:16315 StreamsLib <> I var

R16318:16319 Coq.Lists.Streams <> hd def

R16321:16321 StreamsLib <> s var

R16487:16508 StreamsLib <> inv_prefix_history_rec thm

R16487:16508 StreamsLib <> inv_prefix_history_rec thm

prf 16585:16603 <> inv_prefix_history'

R16623:16623 StreamsLib <> A var

R16644:16644 StreamsLib <> A var

R16639:16639 StreamsLib <> A var

R16660:16665 Coq.Lists.Streams <> Stream coind

R16667:16667 StreamsLib <> A var

R16743:16748 Coq.Lists.Streams <> ForAll coind

R16790:16796 StreamsLib <> history def

R16798:16798 StreamsLib <> s var

R16761:16766 StreamsLib <> prefix def

R16775:16777 Coq.Init.Datatypes <> fst def

R16780:16781 Coq.Lists.Streams <> hd def

R16783:16784 StreamsLib <> s' var

R16772:16772 StreamsLib <> k var

R16770:16770 StreamsLib <> T var

R16768:16768 StreamsLib <> I var

R16684:16689 Coq.Lists.Streams <> ForAll coind

R16726:16726 StreamsLib <> s var

R16702:16702 StreamsLib <> T var

R16713:16714 Coq.Lists.Streams <> hd def

R16717:16718 Coq.Lists.Streams <> tl def

R16720:16721 StreamsLib <> s' var

R16705:16706 Coq.Lists.Streams <> hd def

R16708:16709 StreamsLib <> s' var

R16672:16672 StreamsLib <> I var

R16675:16676 Coq.Lists.Streams <> hd def

R16678:16678 StreamsLib <> s var

R16836:16848 StreamsLib <> necessitation def

R16836:16848 StreamsLib <> necessitation def

R16878:16889 StreamsLib <> ForAll_apply def

R16878:16889 StreamsLib <> ForAll_apply def

R16912:16929 StreamsLib <> inv_prefix_history thm

R16942:16942 Coq.Init.Datatypes <> S constr

R16945:16945 Coq.Init.Datatypes <> S constr

R16939:16939 StreamsLib <> n var

R16937:16937 StreamsLib <> i var

R16912:16929 StreamsLib <> inv_prefix_history thm

R16942:16942 Coq.Init.Datatypes <> S constr

R16945:16945 Coq.Init.Datatypes <> S constr

R16939:16939 StreamsLib <> n var

R16937:16937 StreamsLib <> i var

R16988:17000 StreamsLib <> necessitation def

R16988:17000 StreamsLib <> necessitation def

R0:-1 StreamsLib <> y var

def 17105:17113 <> effective

R17131:17138 Coq.Relations.Relation_Definitions <> relation def

R17140:17140 StreamsLib <> A var

R17161:17162 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not

R17170:17176 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not

R17186:17187 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not

R17163:17163 StreamsLib <> r var

R17168:17169 StreamsLib <> a2 var

R17165:17166 StreamsLib <> a1 var

R17177:17178 Coq.Init.Logic <> :type_scope:'~'_x not

R17179:17179 StreamsLib <> r var

R17184:17185 StreamsLib <> a2 var

R17181:17182 StreamsLib <> a1 var

def 17202:17208 <> lift_hd

R17226:17233 Coq.Relations.Relation_Definitions <> relation def

R17235:17235 StreamsLib <> A var

R17240:17247 Coq.Relations.Relation_Definitions <> relation def

R17250:17255 Coq.Lists.Streams <> Stream coind

R17257:17257 StreamsLib <> A var

R17284:17284 StreamsLib <> r var

R17295:17296 Coq.Lists.Streams <> hd def

R17298:17299 StreamsLib <> s2 var

R17287:17288 Coq.Lists.Streams <> hd def

R17290:17291 StreamsLib <> s1 var

prf 17312:17328 <> lift_hd_effective

R17355:17362 Coq.Relations.Relation_Definitions <> relation def

R17364:17364 StreamsLib <> A var

R17384:17392 StreamsLib <> effective def

R17395:17401 StreamsLib <> lift_hd def

R17403:17403 StreamsLib <> r var

R17369:17377 StreamsLib <> effective def

R17379:17379 StreamsLib <> r var

R17421:17429 StreamsLib <> effective def

R17432:17438 StreamsLib <> lift_hd def

sec 17522:17531 <> FixedPoint

var 17544:17544 FixedPoint A

var 17563:17567 FixedPoint union

R17581:17581 StreamsLib <> FixedPoint.A var

R17576:17576 StreamsLib <> FixedPoint.A var

R17571:17571 StreamsLib <> FixedPoint.A var

var 17594:17595 FixedPoint le

R17599:17606 Coq.Relations.Relation_Definitions <> relation def

R17608:17608 StreamsLib <> FixedPoint.A var

var 17623:17629 FixedPoint le_mono

R17645:17646 StreamsLib <> FixedPoint.le var

R17651:17655 StreamsLib <> FixedPoint.union var

R17659:17659 StreamsLib <> y var

R17657:17657 StreamsLib <> x var

R17648:17648 StreamsLib <> x var

var 17675:17680 FixedPoint le_eff

R17684:17692 StreamsLib <> effective def

R17694:17695 StreamsLib <> FixedPoint.le var

def 17710:17711 <> gt

R17726:17729 Coq.Init.Logic <> :type_scope:x_'/\'_x not

R17720:17721 StreamsLib <> FixedPoint.le var

R17725:17725 StreamsLib <> x var

R17723:17723 StreamsLib <> y var

R17730:17731 Coq.Init.Logic <> :type_scope:'~'_x not

R17732:17733 StreamsLib <> FixedPoint.le var

R17737:17737 StreamsLib <> y var

R17735:17735 StreamsLib <> x var

var 17752:17756 FixedPoint gt_wf

R17760:17771 Coq.Init.Wf <> well_founded def

R17773:17774 StreamsLib <> gt def

fix 17795:17800 <> rec_hd

R17819:17824 Coq.Lists.Streams <> Stream coind

R17826:17826 StreamsLib <> FixedPoint.A var

R17807:17812 Coq.Lists.Streams <> Stream coind

R17814:17814 StreamsLib <> FixedPoint.A var

R17834:17839 Coq.Lists.Streams <> Stream coind

R17841:17841 StreamsLib <> FixedPoint.A var

R17868:17873 Coq.Lists.Streams <> Stream coind

R17875:17875 StreamsLib <> FixedPoint.A var

R17850:17856 StreamsLib <> lift_hd def

R17858:17859 StreamsLib <> gt def

R17891:17895 StreamsLib <> apply def

R17898:17902 StreamsLib <> apply def

R17905:17908 StreamsLib <> lift def

R17910:17914 StreamsLib <> FixedPoint.union var