DIGEST 3e03a7b5b5c26232f0f3e8f10219c975
FNaturelle
R15:23 Coq.Logic.Classical <> <> lib
R97:100 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R97:100 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R218:221 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R218:221 Coq.Init.Logic <> ::type_scope:x_'->'_x not
prf 278:285 <> E_imp_th
R314:314 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R325:329 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R333:336 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R337:339 Naturelle <> psi var
R330:332 Naturelle <> phi var
R318:321 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R322:324 Naturelle <> psi var
R315:317 Naturelle <> phi var
R443:450 Naturelle <> E_imp_th thm
R521:528 Naturelle <> E_imp_th thm
prf 816:826 <> E_forall_th
R856:859 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R855:855 Naturelle <> A var
R869:869 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R885:889 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R890:892 Naturelle <> phi var
R894:894 Naturelle <> a var
R880:882 Naturelle <> phi var
R884:884 Naturelle <> x var
R996:1006 Naturelle <> E_forall_th thm
R1086:1089 Coq.Init.Logic <> ::type_scope:x_'/\'_x not
R1086:1089 Coq.Init.Logic <> ::type_scope:x_'/\'_x not
R1105:1108 Coq.Init.Logic <> conj constr
prf 1157:1165 <> E_et_g_th
R1194:1194 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1205:1209 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1210:1212 Naturelle <> phi var
R1198:1201 Coq.Init.Logic <> ::type_scope:x_'/\'_x not
R1195:1197 Naturelle <> phi var
R1202:1204 Naturelle <> psi var
R1352:1360 Naturelle <> E_et_g_th thm
R1432:1440 Naturelle <> E_et_g_th thm
prf 1465:1473 <> E_et_d_th
R1502:1502 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1513:1517 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1518:1520 Naturelle <> psi var
R1506:1509 Coq.Init.Logic <> ::type_scope:x_'/\'_x not
R1503:1505 Naturelle <> phi var
R1510:1512 Naturelle <> psi var
R1662:1670 Naturelle <> E_et_d_th thm
R1743:1751 Naturelle <> E_et_d_th thm
prf 1776:1782 <> E_ou_th
R1815:1815 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1826:1830 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1831:1831 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1842:1846 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1847:1847 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1858:1862 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1863:1865 Naturelle <> chi var
R1851:1854 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1855:1857 Naturelle <> chi var
R1848:1850 Naturelle <> psi var
R1835:1838 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1839:1841 Naturelle <> chi var
R1832:1834 Naturelle <> phi var
R1819:1822 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R1816:1818 Naturelle <> phi var
R1823:1825 Naturelle <> psi var
R2042:2048 Naturelle <> E_ou_th thm
R2124:2130 Naturelle <> E_ou_th thm
R2194:2197 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R2194:2197 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R2213:2221 Coq.Init.Logic <> or_introl constr
R2305:2308 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R2305:2308 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R2324:2332 Coq.Init.Logic <> or_intror constr
R2416:2423 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2430:2433 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2439:2439 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2438:2438 Naturelle <> x var
R2416:2423 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2430:2433 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2439:2439 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2438:2438 Naturelle <> x var
R2453:2460 Coq.Init.Logic <> ex_intro constr
R2561:2568 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2575:2578 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2584:2584 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2583:2583 Naturelle <> x var
R2561:2568 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2575:2578 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2584:2584 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2583:2583 Naturelle <> x var
R2597:2604 Coq.Init.Logic <> ex_intro constr
prf 2669:2679 <> E_exists_th
R2709:2712 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2708:2708 Naturelle <> A var
R2733:2733 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2749:2753 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2754:2754 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2777:2781 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2782:2784 Naturelle <> chi var
R2770:2773 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2774:2776 Naturelle <> chi var
R2765:2767 Naturelle <> phi var
R2769:2769 Naturelle <> a var
R2734:2740 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2742:2743 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R2744:2746 Naturelle <> phi var
R2748:2748 Naturelle <> x var
R2963:2973 Naturelle <> E_exists_th thm
R3083:3085 Coq.Init.Logic <> not def
R3116:3120 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R3132:3132 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R3123:3126 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3127:3131 Coq.Init.Logic <> False ind
R3116:3120 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R3132:3132 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R3123:3126 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3127:3131 Coq.Init.Logic <> False ind
R3145:3151 Coq.Logic.Classical_Prop <> classic prfax
prf 3209:3218 <> E_antiT_th
R3248:3251 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3252:3254 Naturelle <> phi var
R3243:3247 Coq.Init.Logic <> False ind
R3340:3349 Naturelle <> E_antiT_th thm
prf 3370:3379 <> I_antiT_th
R3407:3410 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3411:3411 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3416:3420 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3421:3425 Coq.Init.Logic <> False ind
R3412:3412 Coq.Init.Logic <> ::type_scope:'~'_x not
R3413:3415 Naturelle <> phi var
R3404:3406 Naturelle <> phi var
R3435:3437 Coq.Init.Logic <> not def
R3551:3555 Coq.Init.Logic <> False ind
R3551:3555 Coq.Init.Logic <> False ind
R3567:3576 Naturelle <> I_antiT_th thm
prf 3598:3605 <> I_non_th
R3630:3630 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3643:3647 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3648:3648 Coq.Init.Logic <> ::type_scope:'~'_x not
R3649:3651 Naturelle <> phi var
R3634:3637 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3638:3642 Coq.Init.Logic <> False ind
R3631:3633 Naturelle <> phi var
R3669:3671 Coq.Init.Logic <> not def
R3730:3731 Coq.Init.Logic <> ::type_scope:'~'_x not
R3730:3731 Coq.Init.Logic <> ::type_scope:'~'_x not
R3745:3752 Naturelle <> I_non_th thm
R3801:3810 Naturelle <> I_antiT_th thm
R3875:3878 Coq.Logic.Classical_Prop <> NNPP thm