| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (977 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (679 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (115 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (114 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Global Index
A
Aas_And_R [constructor, in Proof.Appsub]Aas_And_L [constructor, in Proof.Appsub]
Aas_Lbl [constructor, in Proof.Appsub]
Aas_Arr [constructor, in Proof.Appsub]
Aas_Refl [constructor, in Proof.Appsub]
add_notin_context [lemma, in Proof.LocallyNameless]
Al [constructor, in Proof.Application]
Alt [constructor, in Proof.Appsub]
And [constructor, in Proof.Language]
Ann [constructor, in Proof.Language]
App [constructor, in Proof.Language]
Application [library]
appsub [inductive, in Proof.Appsub]
Appsub [library]
appsub_iso_l [lemma, in Proof.Appsub]
appsub_iso_v [lemma, in Proof.Appsub]
appsub_iso_l2 [lemma, in Proof.Appsub]
appsub_iso_v2 [lemma, in Proof.Appsub]
appsub_iso_v1 [lemma, in Proof.Appsub]
appsub_split_inversion [lemma, in Proof.Appsub]
appsub_determinism [lemma, in Proof.Appsub]
appsub_to_auxas [lemma, in Proof.Appsub]
arg [inductive, in Proof.Appsub]
Arr [constructor, in Proof.Language]
As_And_P [constructor, in Proof.Appsub]
As_And_R [constructor, in Proof.Appsub]
As_And_L [constructor, in Proof.Appsub]
As_Lbl [constructor, in Proof.Appsub]
As_Arr [constructor, in Proof.Appsub]
As_Refl [constructor, in Proof.Appsub]
atype [inductive, in Proof.Application]
atype_determinism [lemma, in Proof.Application]
At_Lbl [constructor, in Proof.Application]
At_Mrg [constructor, in Proof.Application]
At_Rcd [constructor, in Proof.Application]
At_Ann [constructor, in Proof.Application]
auxas [inductive, in Proof.Appsub]
auxas_not_and [lemma, in Proof.Appsub]
auxas_iso_l2 [lemma, in Proof.Appsub]
auxas_iso_v2 [lemma, in Proof.Appsub]
auxas_iso_v1 [lemma, in Proof.Appsub]
auxas_false [lemma, in Proof.Appsub]
Av [constructor, in Proof.Application]
Avt [constructor, in Proof.Appsub]
A1:12 [binder, in Proof.Application]
A1:17 [binder, in Proof.Subtyping.Splitable]
A1:189 [binder, in Proof.Appsub]
A1:20 [binder, in Proof.Subtyping.Splitable]
A1:23 [binder, in Proof.Subtyping.Splitable]
A1:26 [binder, in Proof.Subtyping.Splitable]
A1:28 [binder, in Proof.Casting]
A1:32 [binder, in Proof.Subtyping.Splitable]
A1:36 [binder, in Proof.Subtyping.Subtyping]
A1:39 [binder, in Proof.Subtyping.Subtyping]
A1:42 [binder, in Proof.Subtyping.Subtyping]
A1:46 [binder, in Proof.Subtyping.Subtyping]
A1:59 [binder, in Proof.Subtyping.Subtyping]
A1:75 [binder, in Proof.Subtyping.Subtyping]
A1:81 [binder, in Proof.Subtyping.Subtyping]
A1:9 [binder, in Proof.Reduction]
A2:10 [binder, in Proof.Reduction]
A2:13 [binder, in Proof.Application]
A2:18 [binder, in Proof.Subtyping.Splitable]
A2:190 [binder, in Proof.Appsub]
A2:21 [binder, in Proof.Subtyping.Splitable]
A2:24 [binder, in Proof.Subtyping.Splitable]
A2:27 [binder, in Proof.Subtyping.Splitable]
A2:29 [binder, in Proof.Casting]
A2:33 [binder, in Proof.Subtyping.Splitable]
A2:37 [binder, in Proof.Subtyping.Subtyping]
A2:40 [binder, in Proof.Subtyping.Subtyping]
A2:43 [binder, in Proof.Subtyping.Subtyping]
A2:47 [binder, in Proof.Subtyping.Subtyping]
A2:60 [binder, in Proof.Subtyping.Subtyping]
A2:76 [binder, in Proof.Subtyping.Subtyping]
A2:82 [binder, in Proof.Subtyping.Subtyping]
A3:28 [binder, in Proof.Subtyping.Splitable]
A4:29 [binder, in Proof.Subtyping.Splitable]
A:102 [binder, in Proof.Application]
A:106 [binder, in Proof.Application]
A:11 [binder, in Proof.Appsub]
A:11 [binder, in Proof.Subtyping.Subtyping]
A:11 [binder, in Proof.Subtyping.Splitable]
A:11 [binder, in Proof.PrincipalTyping]
A:112 [binder, in Proof.Application]
A:118 [binder, in Proof.Application]
A:12 [binder, in Proof.Typing]
A:124 [binder, in Proof.Application]
A:128 [binder, in Proof.Application]
A:134 [binder, in Proof.Application]
A:137 [binder, in Proof.Application]
A:14 [binder, in Proof.Appsub]
A:14 [binder, in Proof.Casting]
A:14 [binder, in Proof.PrincipalTyping]
A:143 [binder, in Proof.Application]
A:15 [binder, in Proof.Value]
A:15 [binder, in Proof.Subtyping.Subtyping]
A:16 [binder, in Proof.Subtyping.Splitable]
A:17 [binder, in Proof.Application]
A:17 [binder, in Proof.PrincipalTyping]
A:18 [binder, in Proof.Subtyping.Subtyping]
A:186 [binder, in Proof.Appsub]
A:19 [binder, in Proof.Typing]
A:19 [binder, in Proof.Reduction]
A:19 [binder, in Proof.Appsub]
A:19 [binder, in Proof.Casting]
A:19 [binder, in Proof.Subtyping.Splitable]
A:191 [binder, in Proof.Appsub]
A:193 [binder, in Proof.Appsub]
A:196 [binder, in Proof.Appsub]
A:198 [binder, in Proof.Appsub]
A:20 [binder, in Proof.Appsub]
A:201 [binder, in Proof.Appsub]
A:204 [binder, in Proof.Appsub]
A:21 [binder, in Proof.Typing]
A:21 [binder, in Proof.Subtyping.Subtyping]
A:22 [binder, in Proof.Reduction]
A:22 [binder, in Proof.Subtyping.Splitable]
A:23 [binder, in Proof.Appsub]
A:23 [binder, in Proof.Casting]
A:24 [binder, in Proof.Typing]
A:24 [binder, in Proof.Value]
A:25 [binder, in Proof.Appsub]
A:25 [binder, in Proof.Subtyping.Splitable]
A:26 [binder, in Proof.Subtyping.Subtyping]
A:27 [binder, in Proof.Casting]
A:28 [binder, in Proof.Application]
A:28 [binder, in Proof.Subtyping.Subtyping]
A:29 [binder, in Proof.Appsub]
A:29 [binder, in Proof.Value]
A:3 [binder, in Proof.Subtyping.Subtyping]
A:3 [binder, in Proof.Subtyping.Splitable]
A:30 [binder, in Proof.Subtyping.Splitable]
A:31 [binder, in Proof.Subtyping.Subtyping]
A:31 [binder, in Proof.Subtyping.Splitable]
A:32 [binder, in Proof.Typing]
A:32 [binder, in Proof.Casting]
A:33 [binder, in Proof.Appsub]
A:34 [binder, in Proof.Subtyping.Subtyping]
A:35 [binder, in Proof.Typing]
A:35 [binder, in Proof.Application]
A:35 [binder, in Proof.Casting]
A:35 [binder, in Proof.Subtyping.Subtyping]
A:37 [binder, in Proof.Casting]
A:37 [binder, in Proof.Value]
A:38 [binder, in Proof.LocallyNameless]
A:38 [binder, in Proof.Appsub]
A:38 [binder, in Proof.Subtyping.Subtyping]
A:4 [binder, in Proof.Casting]
A:4 [binder, in Proof.Subtyping.Subtyping]
A:41 [binder, in Proof.Typing]
A:41 [binder, in Proof.Appsub]
A:41 [binder, in Proof.Casting]
A:41 [binder, in Proof.Subtyping.Subtyping]
A:42 [binder, in Proof.Application]
A:44 [binder, in Proof.Typing]
A:44 [binder, in Proof.Appsub]
A:44 [binder, in Proof.Subtyping.Subtyping]
A:45 [binder, in Proof.Casting]
A:45 [binder, in Proof.Value]
A:47 [binder, in Proof.Typing]
A:48 [binder, in Proof.Typing]
A:48 [binder, in Proof.Reduction]
A:48 [binder, in Proof.Appsub]
A:48 [binder, in Proof.Subtyping.Subtyping]
A:5 [binder, in Proof.Reduction]
A:5 [binder, in Proof.Appsub]
A:5 [binder, in Proof.PrincipalTyping]
A:5 [binder, in Proof.Language]
A:51 [binder, in Proof.Value]
A:52 [binder, in Proof.Reduction]
A:52 [binder, in Proof.Application]
A:54 [binder, in Proof.Subtyping.Subtyping]
A:55 [binder, in Proof.Reduction]
A:55 [binder, in Proof.Appsub]
A:57 [binder, in Proof.Subtyping.Subtyping]
A:58 [binder, in Proof.Reduction]
A:58 [binder, in Proof.Appsub]
A:58 [binder, in Proof.Value]
A:58 [binder, in Proof.Subtyping.Subtyping]
A:6 [binder, in Proof.Appsub]
A:6 [binder, in Proof.Application]
A:6 [binder, in Proof.Casting]
A:6 [binder, in Proof.Value]
A:6 [binder, in Proof.Subtyping.Splitable]
A:60 [binder, in Proof.Value]
A:61 [binder, in Proof.Subtyping.Subtyping]
A:63 [binder, in Proof.Appsub]
A:63 [binder, in Proof.Application]
A:64 [binder, in Proof.Subtyping.Subtyping]
A:65 [binder, in Proof.Subtyping.Subtyping]
A:66 [binder, in Proof.Appsub]
A:66 [binder, in Proof.Subtyping.Subtyping]
A:68 [binder, in Proof.Application]
A:69 [binder, in Proof.Appsub]
A:71 [binder, in Proof.Subtyping.Subtyping]
A:73 [binder, in Proof.Subtyping.Subtyping]
A:74 [binder, in Proof.Appsub]
A:77 [binder, in Proof.Reduction]
A:78 [binder, in Proof.Application]
A:79 [binder, in Proof.Appsub]
A:8 [binder, in Proof.Reduction]
A:8 [binder, in Proof.Subtyping.Subtyping]
A:8 [binder, in Proof.PrincipalTyping]
A:80 [binder, in Proof.Subtyping.Subtyping]
A:83 [binder, in Proof.Application]
A:85 [binder, in Proof.Appsub]
A:86 [binder, in Proof.Subtyping.Subtyping]
A:89 [binder, in Proof.Application]
A:89 [binder, in Proof.Subtyping.Subtyping]
A:9 [binder, in Proof.Typing]
A:9 [binder, in Proof.Appsub]
A:9 [binder, in Proof.Application]
A:9 [binder, in Proof.Subtyping.Splitable]
A:90 [binder, in Proof.Appsub]
A:91 [binder, in Proof.Subtyping.Subtyping]
A:93 [binder, in Proof.Appsub]
A:93 [binder, in Proof.Subtyping.Subtyping]
A:95 [binder, in Proof.Subtyping.Subtyping]
A:97 [binder, in Proof.Application]
A:97 [binder, in Proof.Subtyping.Subtyping]
B
Bvar [constructor, in Proof.Language]B1:13 [binder, in Proof.Subtyping.Subtyping]
B1:13 [binder, in Proof.Subtyping.Splitable]
B1:45 [binder, in Proof.Appsub]
B1:50 [binder, in Proof.Subtyping.Subtyping]
B1:51 [binder, in Proof.Appsub]
B1:52 [binder, in Proof.Value]
B1:78 [binder, in Proof.Subtyping.Subtyping]
B1:84 [binder, in Proof.Subtyping.Subtyping]
B2:14 [binder, in Proof.Subtyping.Subtyping]
B2:14 [binder, in Proof.Subtyping.Splitable]
B2:46 [binder, in Proof.Appsub]
B2:51 [binder, in Proof.Subtyping.Subtyping]
B2:52 [binder, in Proof.Appsub]
B2:53 [binder, in Proof.Value]
B2:79 [binder, in Proof.Subtyping.Subtyping]
B2:85 [binder, in Proof.Subtyping.Subtyping]
B:10 [binder, in Proof.Subtyping.Splitable]
B:107 [binder, in Proof.Application]
B:114 [binder, in Proof.Application]
B:119 [binder, in Proof.Application]
B:12 [binder, in Proof.Appsub]
B:12 [binder, in Proof.Subtyping.Subtyping]
B:12 [binder, in Proof.Subtyping.Splitable]
B:125 [binder, in Proof.Application]
B:129 [binder, in Proof.Application]
B:13 [binder, in Proof.Typing]
B:138 [binder, in Proof.Application]
B:15 [binder, in Proof.Appsub]
B:15 [binder, in Proof.PrincipalTyping]
B:16 [binder, in Proof.Subtyping.Subtyping]
B:18 [binder, in Proof.Application]
B:18 [binder, in Proof.PrincipalTyping]
B:19 [binder, in Proof.Subtyping.Subtyping]
B:195 [binder, in Proof.Appsub]
B:200 [binder, in Proof.Appsub]
B:203 [binder, in Proof.Appsub]
B:21 [binder, in Proof.Appsub]
B:22 [binder, in Proof.Subtyping.Subtyping]
B:25 [binder, in Proof.Typing]
B:25 [binder, in Proof.Value]
B:26 [binder, in Proof.Appsub]
B:27 [binder, in Proof.Subtyping.Subtyping]
B:29 [binder, in Proof.Application]
B:29 [binder, in Proof.Subtyping.Subtyping]
B:30 [binder, in Proof.Appsub]
B:32 [binder, in Proof.Subtyping.Subtyping]
B:33 [binder, in Proof.Typing]
B:34 [binder, in Proof.Appsub]
B:36 [binder, in Proof.Typing]
B:36 [binder, in Proof.Application]
B:38 [binder, in Proof.Casting]
B:39 [binder, in Proof.LocallyNameless]
B:39 [binder, in Proof.Appsub]
B:4 [binder, in Proof.Subtyping.Splitable]
B:42 [binder, in Proof.Typing]
B:42 [binder, in Proof.Appsub]
B:43 [binder, in Proof.Application]
B:45 [binder, in Proof.Subtyping.Subtyping]
B:46 [binder, in Proof.Casting]
B:49 [binder, in Proof.Typing]
B:49 [binder, in Proof.Reduction]
B:49 [binder, in Proof.Appsub]
B:49 [binder, in Proof.Subtyping.Subtyping]
B:5 [binder, in Proof.Subtyping.Subtyping]
B:55 [binder, in Proof.Subtyping.Subtyping]
B:56 [binder, in Proof.Appsub]
B:59 [binder, in Proof.Appsub]
B:6 [binder, in Proof.Reduction]
B:6 [binder, in Proof.PrincipalTyping]
B:61 [binder, in Proof.Value]
B:62 [binder, in Proof.Subtyping.Subtyping]
B:64 [binder, in Proof.Appsub]
B:67 [binder, in Proof.Subtyping.Subtyping]
B:7 [binder, in Proof.Appsub]
B:7 [binder, in Proof.Casting]
B:7 [binder, in Proof.Value]
B:70 [binder, in Proof.Appsub]
B:74 [binder, in Proof.Subtyping.Subtyping]
B:75 [binder, in Proof.Appsub]
B:77 [binder, in Proof.Subtyping.Subtyping]
B:80 [binder, in Proof.Appsub]
B:83 [binder, in Proof.Subtyping.Subtyping]
B:86 [binder, in Proof.Appsub]
B:87 [binder, in Proof.Subtyping.Subtyping]
B:9 [binder, in Proof.Subtyping.Subtyping]
B:90 [binder, in Proof.Application]
B:90 [binder, in Proof.Subtyping.Subtyping]
B:91 [binder, in Proof.Appsub]
B:92 [binder, in Proof.Subtyping.Subtyping]
B:94 [binder, in Proof.Subtyping.Subtyping]
B:96 [binder, in Proof.Subtyping.Subtyping]
B:98 [binder, in Proof.Application]
B:98 [binder, in Proof.Subtyping.Subtyping]
C
casting [inductive, in Proof.Casting]Casting [library]
casting_preservation [lemma, in Proof.Casting]
casting_progress [lemma, in Proof.Casting]
casting_progress' [lemma, in Proof.Casting]
casting_value [lemma, in Proof.Casting]
casting_lc [lemma, in Proof.Casting]
Chk [constructor, in Proof.Typing]
ctx [definition, in Proof.Language]
Ct_And [constructor, in Proof.Casting]
Ct_Mrg_R [constructor, in Proof.Casting]
Ct_Mrg_L [constructor, in Proof.Casting]
Ct_Rcd [constructor, in Proof.Casting]
Ct_Lam [constructor, in Proof.Casting]
Ct_Top [constructor, in Proof.Casting]
Ct_Lit [constructor, in Proof.Casting]
C1:36 [binder, in Proof.Appsub]
C1:53 [binder, in Proof.Appsub]
C2:37 [binder, in Proof.Appsub]
C2:54 [binder, in Proof.Appsub]
C:108 [binder, in Proof.Application]
C:120 [binder, in Proof.Application]
C:130 [binder, in Proof.Application]
C:17 [binder, in Proof.Subtyping.Subtyping]
C:19 [binder, in Proof.Application]
C:20 [binder, in Proof.Subtyping.Subtyping]
C:22 [binder, in Proof.Appsub]
C:23 [binder, in Proof.Subtyping.Subtyping]
C:26 [binder, in Proof.Typing]
C:28 [binder, in Proof.Appsub]
C:30 [binder, in Proof.Subtyping.Subtyping]
C:32 [binder, in Proof.Appsub]
C:33 [binder, in Proof.Subtyping.Subtyping]
C:47 [binder, in Proof.Casting]
C:50 [binder, in Proof.Appsub]
C:6 [binder, in Proof.Subtyping.Subtyping]
C:60 [binder, in Proof.Appsub]
C:68 [binder, in Proof.Subtyping.Subtyping]
C:71 [binder, in Proof.Appsub]
C:78 [binder, in Proof.Appsub]
C:8 [binder, in Proof.Appsub]
C:8 [binder, in Proof.Casting]
C:81 [binder, in Proof.Appsub]
C:88 [binder, in Proof.Subtyping.Subtyping]
C:89 [binder, in Proof.Appsub]
C:91 [binder, in Proof.Application]
D
dec_sub [axiom, in Proof.Appsub]dir:56 [binder, in Proof.Reduction]
dir:59 [binder, in Proof.Reduction]
dir:64 [binder, in Proof.Application]
dir:69 [binder, in Proof.Application]
dir:78 [binder, in Proof.Reduction]
dir:79 [binder, in Proof.Application]
dir:92 [binder, in Proof.Application]
D:109 [binder, in Proof.Application]
D:20 [binder, in Proof.Application]
D:24 [binder, in Proof.Subtyping.Subtyping]
D:62 [binder, in Proof.Appsub]
D:7 [binder, in Proof.Subtyping.Subtyping]
D:73 [binder, in Proof.Appsub]
D:84 [binder, in Proof.Appsub]
D:9 [binder, in Proof.Casting]
D:93 [binder, in Proof.Application]
E
e':21 [binder, in Proof.Reduction]e':31 [binder, in Proof.Reduction]
e':33 [binder, in Proof.Reduction]
e':44 [binder, in Proof.Reduction]
e':47 [binder, in Proof.Reduction]
e':51 [binder, in Proof.Reduction]
e':54 [binder, in Proof.Reduction]
e':60 [binder, in Proof.Reduction]
e':73 [binder, in Proof.Reduction]
e':76 [binder, in Proof.Reduction]
e1':24 [binder, in Proof.Reduction]
e1':36 [binder, in Proof.Reduction]
e1:10 [binder, in Proof.Application]
e1:10 [binder, in Proof.Value]
e1:12 [binder, in Proof.Value]
e1:12 [binder, in Proof.PrincipalTyping]
e1:17 [binder, in Proof.LocallyNameless]
e1:23 [binder, in Proof.Reduction]
e1:27 [binder, in Proof.Typing]
e1:35 [binder, in Proof.Reduction]
e1:37 [binder, in Proof.Typing]
e1:40 [binder, in Proof.LocallyNameless]
e1:46 [binder, in Proof.Application]
e1:46 [binder, in Proof.Value]
e1:48 [binder, in Proof.Value]
e1:73 [binder, in Proof.Application]
e2':28 [binder, in Proof.Reduction]
e2':40 [binder, in Proof.Reduction]
e2:11 [binder, in Proof.Application]
e2:11 [binder, in Proof.Value]
e2:13 [binder, in Proof.Value]
e2:13 [binder, in Proof.PrincipalTyping]
e2:18 [binder, in Proof.LocallyNameless]
e2:25 [binder, in Proof.Reduction]
e2:27 [binder, in Proof.Reduction]
e2:28 [binder, in Proof.Typing]
e2:37 [binder, in Proof.Reduction]
e2:38 [binder, in Proof.Typing]
e2:39 [binder, in Proof.Reduction]
e2:41 [binder, in Proof.LocallyNameless]
e2:47 [binder, in Proof.Application]
e2:47 [binder, in Proof.Value]
e2:49 [binder, in Proof.Value]
e2:74 [binder, in Proof.Application]
E:10 [binder, in Proof.Casting]
e:10 [binder, in Proof.PrincipalTyping]
e:101 [binder, in Proof.Application]
e:105 [binder, in Proof.Application]
e:11 [binder, in Proof.Casting]
e:113 [binder, in Proof.Application]
e:117 [binder, in Proof.Application]
e:123 [binder, in Proof.Application]
e:13 [binder, in Proof.Reduction]
e:131 [binder, in Proof.Application]
e:135 [binder, in Proof.Application]
e:14 [binder, in Proof.Typing]
e:14 [binder, in Proof.Value]
e:14 [binder, in Proof.Language]
e:140 [binder, in Proof.Application]
e:144 [binder, in Proof.Application]
e:16 [binder, in Proof.Reduction]
e:16 [binder, in Proof.LocallyNameless]
e:16 [binder, in Proof.Value]
e:16 [binder, in Proof.PrincipalTyping]
e:17 [binder, in Proof.Typing]
e:17 [binder, in Proof.Language]
e:18 [binder, in Proof.Value]
e:2 [binder, in Proof.LocallyNameless]
e:20 [binder, in Proof.Reduction]
e:22 [binder, in Proof.Typing]
e:22 [binder, in Proof.Language]
e:23 [binder, in Proof.Application]
e:23 [binder, in Proof.Value]
e:25 [binder, in Proof.LocallyNameless]
e:25 [binder, in Proof.Language]
e:28 [binder, in Proof.LocallyNameless]
e:28 [binder, in Proof.Value]
e:30 [binder, in Proof.Typing]
e:30 [binder, in Proof.Reduction]
e:31 [binder, in Proof.LocallyNameless]
e:32 [binder, in Proof.Reduction]
e:32 [binder, in Proof.Application]
e:35 [binder, in Proof.LocallyNameless]
e:36 [binder, in Proof.LocallyNameless]
e:36 [binder, in Proof.Value]
e:39 [binder, in Proof.Application]
e:4 [binder, in Proof.Reduction]
e:4 [binder, in Proof.PrincipalTyping]
e:40 [binder, in Proof.Typing]
e:42 [binder, in Proof.Reduction]
e:43 [binder, in Proof.Reduction]
e:44 [binder, in Proof.Value]
e:46 [binder, in Proof.Typing]
e:46 [binder, in Proof.Reduction]
e:5 [binder, in Proof.Application]
e:5 [binder, in Proof.Value]
e:50 [binder, in Proof.Typing]
e:50 [binder, in Proof.Reduction]
e:50 [binder, in Proof.Value]
e:53 [binder, in Proof.Reduction]
e:55 [binder, in Proof.Application]
e:55 [binder, in Proof.Value]
e:56 [binder, in Proof.Value]
e:57 [binder, in Proof.Reduction]
e:58 [binder, in Proof.Application]
e:59 [binder, in Proof.Value]
E:60 [binder, in Proof.Application]
e:62 [binder, in Proof.Application]
E:65 [binder, in Proof.Application]
e:67 [binder, in Proof.Application]
e:7 [binder, in Proof.Application]
e:7 [binder, in Proof.PrincipalTyping]
E:70 [binder, in Proof.Application]
e:71 [binder, in Proof.Application]
e:72 [binder, in Proof.Reduction]
e:74 [binder, in Proof.Reduction]
e:75 [binder, in Proof.Reduction]
e:75 [binder, in Proof.Value]
e:76 [binder, in Proof.Value]
e:77 [binder, in Proof.Application]
e:8 [binder, in Proof.Language]
e:80 [binder, in Proof.Application]
E:85 [binder, in Proof.Application]
e:88 [binder, in Proof.Application]
e:9 [binder, in Proof.LocallyNameless]
e:96 [binder, in Proof.Application]
F
Fld [constructor, in Proof.Language]fv [definition, in Proof.Language]
Fvar [constructor, in Proof.Language]
fv_open_lower [lemma, in Proof.LocallyNameless]
fv_in_dom [lemma, in Proof.Application]
fv_open_lower [lemma, in Proof.Application]
f:11 [binder, in Proof.Reduction]
f:126 [binder, in Proof.Application]
F:61 [binder, in Proof.Application]
F:66 [binder, in Proof.Application]
F:84 [binder, in Proof.Application]
G
G:59 [binder, in Proof.Application]H
H1:82 [binder, in Proof.Appsub]H2:83 [binder, in Proof.Appsub]
H:57 [binder, in Proof.Appsub]
H:61 [binder, in Proof.Appsub]
H:65 [binder, in Proof.Appsub]
H:68 [binder, in Proof.Appsub]
H:72 [binder, in Proof.Appsub]
H:76 [binder, in Proof.Appsub]
H:87 [binder, in Proof.Appsub]
I
Inf [constructor, in Proof.Typing]Int [constructor, in Proof.Language]
isomorphic_spec [definition, in Proof.Subtyping.Subtyping]
isosub [inductive, in Proof.Subtyping.Subtyping]
isosub_to_sub2 [lemma, in Proof.Subtyping.Subtyping]
isosub_to_sub1 [lemma, in Proof.Subtyping.Subtyping]
isosub_sound [lemma, in Proof.Subtyping.Subtyping]
isosub_transitivity [lemma, in Proof.Subtyping.Subtyping]
isosub_inv_splitable [lemma, in Proof.Subtyping.Subtyping]
Isub_And [constructor, in Proof.Subtyping.Subtyping]
Isub_Rcd [constructor, in Proof.Subtyping.Subtyping]
Isub_Refl [constructor, in Proof.Subtyping.Subtyping]
i:11 [binder, in Proof.Language]
i:12 [binder, in Proof.LocallyNameless]
i:45 [binder, in Proof.Reduction]
J
j:10 [binder, in Proof.LocallyNameless]K
k:14 [binder, in Proof.LocallyNameless]k:20 [binder, in Proof.Language]
k:21 [binder, in Proof.LocallyNameless]
k:42 [binder, in Proof.LocallyNameless]
k:75 [binder, in Proof.Application]
L
label [definition, in Proof.Language]Lam [constructor, in Proof.Language]
Language [library]
lc [inductive, in Proof.Value]
lc_inv_rcd [lemma, in Proof.Value]
lc_inv_lam [lemma, in Proof.Value]
lc_inv_merge_r [lemma, in Proof.Value]
lc_inv_merge_l [lemma, in Proof.Value]
lc_inv_anno [lemma, in Proof.Value]
lc_value [lemma, in Proof.Value]
lc_pvalue [lemma, in Proof.Value]
Lc_Prj [constructor, in Proof.Value]
Lc_Fld [constructor, in Proof.Value]
Lc_Ann [constructor, in Proof.Value]
Lc_Mrg [constructor, in Proof.Value]
Lc_App [constructor, in Proof.Value]
Lc_Lam [constructor, in Proof.Value]
Lc_Var [constructor, in Proof.Value]
Lc_Lit [constructor, in Proof.Value]
Lit [constructor, in Proof.Language]
LocallyNameless [library]
L:10 [binder, in Proof.Typing]
l:10 [binder, in Proof.Appsub]
l:10 [binder, in Proof.Subtyping.Subtyping]
l:100 [binder, in Proof.Application]
l:116 [binder, in Proof.Application]
l:121 [binder, in Proof.Application]
l:139 [binder, in Proof.Application]
l:14 [binder, in Proof.Reduction]
l:14 [binder, in Proof.Application]
l:142 [binder, in Proof.Application]
l:15 [binder, in Proof.Casting]
l:15 [binder, in Proof.Subtyping.Splitable]
l:17 [binder, in Proof.Value]
l:18 [binder, in Proof.Typing]
l:19 [binder, in Proof.Value]
l:24 [binder, in Proof.Appsub]
l:25 [binder, in Proof.Application]
l:25 [binder, in Proof.Subtyping.Subtyping]
l:29 [binder, in Proof.Reduction]
l:30 [binder, in Proof.Value]
l:31 [binder, in Proof.Typing]
l:34 [binder, in Proof.Reduction]
l:38 [binder, in Proof.Value]
l:5 [binder, in Proof.Subtyping.Splitable]
l:54 [binder, in Proof.Value]
l:56 [binder, in Proof.Subtyping.Subtyping]
l:62 [binder, in Proof.Value]
l:63 [binder, in Proof.Subtyping.Subtyping]
l:67 [binder, in Proof.Appsub]
l:68 [binder, in Proof.Value]
l:72 [binder, in Proof.Subtyping.Subtyping]
l:77 [binder, in Proof.Appsub]
l:8 [binder, in Proof.Application]
L:8 [binder, in Proof.Value]
l:88 [binder, in Proof.Appsub]
l:9 [binder, in Proof.PrincipalTyping]
M
mode [inductive, in Proof.Typing]modusponens [lemma, in Proof.Tactical]
Mrg [constructor, in Proof.Language]
multi [inductive, in Proof.Reduction]
multistep [abbreviation, in Proof.Reduction]
multi_step [constructor, in Proof.Reduction]
multi_refl [constructor, in Proof.Reduction]
N
normal_form [definition, in Proof.Reduction]n:22 [binder, in Proof.Value]
n:3 [binder, in Proof.Reduction]
n:3 [binder, in Proof.Casting]
n:3 [binder, in Proof.Value]
n:3 [binder, in Proof.PrincipalTyping]
n:6 [binder, in Proof.Typing]
O
open [definition, in Proof.Language]open_abs [lemma, in Proof.LocallyNameless]
open_rec_lc [lemma, in Proof.LocallyNameless]
open_rec_lc_core [lemma, in Proof.LocallyNameless]
open_rec [definition, in Proof.Language]
ordinary [inductive, in Proof.Subtyping.Splitable]
ordinary_decidable [lemma, in Proof.Subtyping.Splitable]
Ord_Rcd [constructor, in Proof.Subtyping.Splitable]
Ord_Arr [constructor, in Proof.Subtyping.Splitable]
Ord_Tnt [constructor, in Proof.Subtyping.Splitable]
Ord_Top [constructor, in Proof.Subtyping.Splitable]
P
papp [inductive, in Proof.Application]papp_progress_l_formal [lemma, in Proof.Application]
papp_progress_l [lemma, in Proof.Application]
papp_progress_v_formal [lemma, in Proof.Application]
papp_progress_v [lemma, in Proof.Application]
papp_preservation_l_formal [lemma, in Proof.Application]
papp_preservation_l [lemma, in Proof.Application]
papp_preservation_v_formal [lemma, in Proof.Application]
papp_preservation_v [lemma, in Proof.Application]
papp_uvalue_l [lemma, in Proof.Application]
papp_uvalue_v [lemma, in Proof.Application]
papp_preservation [section, in Proof.Application]
papp_lc_l [lemma, in Proof.Application]
papp_lc_v [lemma, in Proof.Application]
Pa_Mrg_P [constructor, in Proof.Application]
Pa_Mrg_R [constructor, in Proof.Application]
Pa_Mrg_L [constructor, in Proof.Application]
Pa_Rcd [constructor, in Proof.Application]
Pa_Lam [constructor, in Proof.Application]
preservation [lemma, in Proof.Reduction]
preservation_gen [lemma, in Proof.Reduction]
preservation_chk [lemma, in Proof.Reduction]
PrincipalTyping [library]
Prj [constructor, in Proof.Language]
progress [lemma, in Proof.Reduction]
proper [inductive, in Proof.Subtyping.Subtyping]
proper_complete [lemma, in Proof.Subtyping.Subtyping]
proper_record [lemma, in Proof.Subtyping.Subtyping]
proper_arrow [lemma, in Proof.Subtyping.Subtyping]
Pr_Spl [constructor, in Proof.Subtyping.Subtyping]
Pr_Rcd [constructor, in Proof.Subtyping.Subtyping]
Pr_Arr [constructor, in Proof.Subtyping.Subtyping]
Pr_Top [constructor, in Proof.Subtyping.Subtyping]
Pr_Int [constructor, in Proof.Subtyping.Subtyping]
psub [definition, in Proof.Appsub]
psub_auxas_false [lemma, in Proof.Appsub]
psub_appsub_false [lemma, in Proof.Appsub]
psub_complete_appsub [lemma, in Proof.Appsub]
psub_sound_auxas [lemma, in Proof.Appsub]
psub_sound_appsub [lemma, in Proof.Appsub]
psub_none_auxas2 [lemma, in Proof.Appsub]
psub_none_auxas1 [lemma, in Proof.Appsub]
ptype [inductive, in Proof.PrincipalTyping]
ptype_determinism [lemma, in Proof.PrincipalTyping]
Pt_Mrg [constructor, in Proof.PrincipalTyping]
Pt_Rcd [constructor, in Proof.PrincipalTyping]
Pt_Ann [constructor, in Proof.PrincipalTyping]
Pt_Arr [constructor, in Proof.PrincipalTyping]
Pt_Int [constructor, in Proof.PrincipalTyping]
pvalue [inductive, in Proof.Value]
pvalue_decidable [lemma, in Proof.Value]
pvalue_and_value [lemma, in Proof.Value]
Pv_Lam [constructor, in Proof.Value]
Pv_Lit [constructor, in Proof.Value]
P:1 [binder, in Proof.Tactical]
p:42 [binder, in Proof.Value]
p:7 [binder, in Proof.Reduction]
Q
Q:2 [binder, in Proof.Tactical]R
Rcd [constructor, in Proof.Language]Reduction [library]
relation [definition, in Proof.Reduction]
R:63 [binder, in Proof.Reduction]
R:71 [binder, in Proof.Reduction]
S
size_term [definition, in Proof.Language]size_type [definition, in Proof.Language]
soundness [lemma, in Proof.Reduction]
splitable [inductive, in Proof.Subtyping.Splitable]
Splitable [library]
splitable_decrease_size [lemma, in Proof.Subtyping.Splitable]
splitable_determinism [lemma, in Proof.Subtyping.Splitable]
splitable_or_ordinary [lemma, in Proof.Subtyping.Splitable]
splitable_not_ordinary [lemma, in Proof.Subtyping.Splitable]
Spl_Rcd [constructor, in Proof.Subtyping.Splitable]
Spl_Arr [constructor, in Proof.Subtyping.Splitable]
Spl_And [constructor, in Proof.Subtyping.Splitable]
step [inductive, in Proof.Reduction]
step_lc [lemma, in Proof.Reduction]
stuck [definition, in Proof.Reduction]
St_Mrg_R [constructor, in Proof.Reduction]
St_Mrg_L [constructor, in Proof.Reduction]
St_Prj_L [constructor, in Proof.Reduction]
St_Rcd [constructor, in Proof.Reduction]
St_App_R [constructor, in Proof.Reduction]
St_App_L [constructor, in Proof.Reduction]
St_Ann [constructor, in Proof.Reduction]
St_Val [constructor, in Proof.Reduction]
St_Prj [constructor, in Proof.Reduction]
St_App [constructor, in Proof.Reduction]
St_Spl [constructor, in Proof.Reduction]
St_Lam [constructor, in Proof.Reduction]
St_Lit [constructor, in Proof.Reduction]
sub [inductive, in Proof.Subtyping.Subtyping]
substitution [definition, in Proof.Language]
substitution_lemma [lemma, in Proof.Application]
subst_notin_fv [lemma, in Proof.LocallyNameless]
subst_intro [lemma, in Proof.LocallyNameless]
subst_lc [lemma, in Proof.LocallyNameless]
subst_open_var [lemma, in Proof.LocallyNameless]
subst_open_rec [lemma, in Proof.LocallyNameless]
subst_neq_var [lemma, in Proof.LocallyNameless]
subst_eq_var [lemma, in Proof.LocallyNameless]
subst_fresh [lemma, in Proof.LocallyNameless]
subst_value [lemma, in Proof.Application]
Subtyping [library]
sub_arrow_int [lemma, in Proof.Subtyping.Subtyping]
sub_transitivity [lemma, in Proof.Subtyping.Subtyping]
sub_inv_splitable_r [lemma, in Proof.Subtyping.Subtyping]
sub_inv_splitable_l [lemma, in Proof.Subtyping.Subtyping]
sub_splitable [lemma, in Proof.Subtyping.Subtyping]
sub_splitable_r [lemma, in Proof.Subtyping.Subtyping]
sub_splitable_l [lemma, in Proof.Subtyping.Subtyping]
sub_reflexivity [lemma, in Proof.Subtyping.Subtyping]
sub_and_r [lemma, in Proof.Subtyping.Subtyping]
sub_and_l [lemma, in Proof.Subtyping.Subtyping]
sub_record [lemma, in Proof.Subtyping.Subtyping]
sub_arrow [lemma, in Proof.Subtyping.Subtyping]
Sub_And_R [constructor, in Proof.Subtyping.Subtyping]
Sub_And_L [constructor, in Proof.Subtyping.Subtyping]
Sub_And [constructor, in Proof.Subtyping.Subtyping]
Sub_Rcd [constructor, in Proof.Subtyping.Subtyping]
Sub_Arr [constructor, in Proof.Subtyping.Subtyping]
Sub_Top [constructor, in Proof.Subtyping.Subtyping]
Sub_Int [constructor, in Proof.Subtyping.Subtyping]
S:13 [binder, in Proof.Appsub]
S:16 [binder, in Proof.Appsub]
S:187 [binder, in Proof.Appsub]
S:188 [binder, in Proof.Appsub]
S:192 [binder, in Proof.Appsub]
S:194 [binder, in Proof.Appsub]
S:197 [binder, in Proof.Appsub]
S:199 [binder, in Proof.Appsub]
S:202 [binder, in Proof.Appsub]
S:205 [binder, in Proof.Appsub]
S:27 [binder, in Proof.Appsub]
S:31 [binder, in Proof.Appsub]
S:35 [binder, in Proof.Appsub]
S:40 [binder, in Proof.Appsub]
S:43 [binder, in Proof.Appsub]
S:47 [binder, in Proof.Appsub]
S:94 [binder, in Proof.Appsub]
T
Tactical [library]TA1:49 [binder, in Proof.Application]
TA2:50 [binder, in Proof.Application]
TA:31 [binder, in Proof.Application]
TA:38 [binder, in Proof.Application]
TA:45 [binder, in Proof.Application]
term [inductive, in Proof.Language]
Top [constructor, in Proof.Language]
type [inductive, in Proof.Language]
typing [inductive, in Proof.Typing]
Typing [library]
typing_chk_sub [lemma, in Proof.Typing]
typing_to_lc [lemma, in Proof.Typing]
typing_to_ptype [lemma, in Proof.Typing]
typing_uniq [lemma, in Proof.Application]
typing_weakening [lemma, in Proof.Application]
typing_weakening_gen [lemma, in Proof.Application]
typing_to_atype [lemma, in Proof.Application]
Ty_Sub [constructor, in Proof.Typing]
Ty_Mrg [constructor, in Proof.Typing]
Ty_Prj [constructor, in Proof.Typing]
Ty_App [constructor, in Proof.Typing]
Ty_Ann [constructor, in Proof.Typing]
Ty_Rcd [constructor, in Proof.Typing]
Ty_Lam [constructor, in Proof.Typing]
Ty_Var [constructor, in Proof.Typing]
Ty_Int [constructor, in Proof.Typing]
T1:44 [binder, in Proof.LocallyNameless]
T2:45 [binder, in Proof.LocallyNameless]
T:11 [binder, in Proof.Typing]
T:16 [binder, in Proof.Typing]
T:20 [binder, in Proof.Typing]
T:23 [binder, in Proof.Typing]
T:29 [binder, in Proof.Typing]
T:34 [binder, in Proof.Typing]
T:39 [binder, in Proof.Typing]
T:45 [binder, in Proof.Typing]
T:5 [binder, in Proof.Typing]
T:51 [binder, in Proof.Typing]
T:7 [binder, in Proof.Typing]
T:72 [binder, in Proof.Application]
T:76 [binder, in Proof.Application]
U
uvalue [inductive, in Proof.Value]uvalue_inv_merge_r [lemma, in Proof.Value]
uvalue_inv_merge_l [lemma, in Proof.Value]
uvalue_inv_rcd [lemma, in Proof.Value]
Uv_Mrg [constructor, in Proof.Value]
Uv_Rcd [constructor, in Proof.Value]
Uv_Ann [constructor, in Proof.Value]
u1:32 [binder, in Proof.Value]
u1:70 [binder, in Proof.Value]
u1:72 [binder, in Proof.Value]
u2:33 [binder, in Proof.Value]
u2:71 [binder, in Proof.Value]
u2:73 [binder, in Proof.Value]
u:13 [binder, in Proof.LocallyNameless]
u:13 [binder, in Proof.Language]
u:15 [binder, in Proof.LocallyNameless]
u:19 [binder, in Proof.LocallyNameless]
u:21 [binder, in Proof.Language]
u:24 [binder, in Proof.LocallyNameless]
u:26 [binder, in Proof.Language]
u:27 [binder, in Proof.LocallyNameless]
u:3 [binder, in Proof.LocallyNameless]
u:30 [binder, in Proof.LocallyNameless]
u:31 [binder, in Proof.Value]
u:34 [binder, in Proof.LocallyNameless]
u:37 [binder, in Proof.LocallyNameless]
u:43 [binder, in Proof.Typing]
u:5 [binder, in Proof.LocallyNameless]
u:69 [binder, in Proof.Value]
u:8 [binder, in Proof.LocallyNameless]
u:82 [binder, in Proof.Application]
V
value [inductive, in Proof.Value]Value [library]
value_no_step [lemma, in Proof.Reduction]
value_decidable [lemma, in Proof.Value]
value_is_uvalue [lemma, in Proof.Value]
value_inv_merge_r [lemma, in Proof.Value]
value_inv_merge_l [lemma, in Proof.Value]
value_inv_rcd [lemma, in Proof.Value]
value_anno_ordinary [lemma, in Proof.Value]
value_and_value_anno [lemma, in Proof.Value]
vl [inductive, in Proof.Application]
vl:104 [binder, in Proof.Application]
vl:30 [binder, in Proof.Application]
vl:37 [binder, in Proof.Application]
vl:44 [binder, in Proof.Application]
vl:48 [binder, in Proof.Application]
vl:54 [binder, in Proof.Application]
vl:57 [binder, in Proof.Application]
vl:95 [binder, in Proof.Application]
V_Mrg [constructor, in Proof.Value]
V_Rcd [constructor, in Proof.Value]
V_Ann [constructor, in Proof.Value]
v':13 [binder, in Proof.Casting]
v':18 [binder, in Proof.Reduction]
v':22 [binder, in Proof.Application]
v':31 [binder, in Proof.Casting]
v':34 [binder, in Proof.Casting]
v':39 [binder, in Proof.Casting]
v':42 [binder, in Proof.Casting]
v':44 [binder, in Proof.Casting]
v1:110 [binder, in Proof.Application]
v1:132 [binder, in Proof.Application]
v1:16 [binder, in Proof.Casting]
v1:20 [binder, in Proof.Casting]
v1:24 [binder, in Proof.Casting]
v1:26 [binder, in Proof.Application]
v1:33 [binder, in Proof.Application]
v1:40 [binder, in Proof.Application]
v1:40 [binder, in Proof.Value]
v1:64 [binder, in Proof.Value]
v1:66 [binder, in Proof.Value]
v2:111 [binder, in Proof.Application]
v2:133 [binder, in Proof.Application]
v2:17 [binder, in Proof.Casting]
v2:21 [binder, in Proof.Casting]
v2:25 [binder, in Proof.Casting]
v2:27 [binder, in Proof.Application]
v2:34 [binder, in Proof.Application]
v2:41 [binder, in Proof.Application]
v2:41 [binder, in Proof.Value]
v2:65 [binder, in Proof.Value]
v2:67 [binder, in Proof.Value]
v:103 [binder, in Proof.Application]
v:11 [binder, in Proof.LocallyNameless]
v:115 [binder, in Proof.Application]
v:12 [binder, in Proof.Reduction]
v:12 [binder, in Proof.Casting]
v:122 [binder, in Proof.Application]
v:127 [binder, in Proof.Application]
v:136 [binder, in Proof.Application]
v:141 [binder, in Proof.Application]
v:15 [binder, in Proof.Reduction]
v:17 [binder, in Proof.Reduction]
v:18 [binder, in Proof.Casting]
v:21 [binder, in Proof.Application]
v:22 [binder, in Proof.Casting]
v:24 [binder, in Proof.Application]
v:26 [binder, in Proof.Reduction]
v:26 [binder, in Proof.Casting]
v:30 [binder, in Proof.Casting]
v:33 [binder, in Proof.Casting]
v:36 [binder, in Proof.Casting]
v:38 [binder, in Proof.Reduction]
v:39 [binder, in Proof.Value]
v:40 [binder, in Proof.Casting]
v:41 [binder, in Proof.Reduction]
v:43 [binder, in Proof.Casting]
v:43 [binder, in Proof.Value]
v:5 [binder, in Proof.Casting]
v:51 [binder, in Proof.Application]
v:53 [binder, in Proof.Application]
v:56 [binder, in Proof.Application]
v:57 [binder, in Proof.Value]
v:63 [binder, in Proof.Value]
v:74 [binder, in Proof.Value]
v:87 [binder, in Proof.Application]
v:94 [binder, in Proof.Application]
v:99 [binder, in Proof.Application]
X
x:1 [binder, in Proof.LocallyNameless]x:15 [binder, in Proof.Typing]
x:20 [binder, in Proof.LocallyNameless]
x:22 [binder, in Proof.LocallyNameless]
x:26 [binder, in Proof.LocallyNameless]
x:27 [binder, in Proof.Language]
x:28 [binder, in Proof.Language]
x:29 [binder, in Proof.LocallyNameless]
x:29 [binder, in Proof.Language]
x:30 [binder, in Proof.Language]
x:32 [binder, in Proof.LocallyNameless]
x:4 [binder, in Proof.LocallyNameless]
x:4 [binder, in Proof.Value]
x:43 [binder, in Proof.LocallyNameless]
x:6 [binder, in Proof.LocallyNameless]
X:61 [binder, in Proof.Reduction]
X:62 [binder, in Proof.Reduction]
x:66 [binder, in Proof.Reduction]
x:67 [binder, in Proof.Reduction]
X:70 [binder, in Proof.Reduction]
x:8 [binder, in Proof.Typing]
x:86 [binder, in Proof.Application]
x:9 [binder, in Proof.Value]
Y
y:23 [binder, in Proof.LocallyNameless]y:33 [binder, in Proof.LocallyNameless]
y:68 [binder, in Proof.Reduction]
y:7 [binder, in Proof.LocallyNameless]
Z
z:12 [binder, in Proof.Language]z:69 [binder, in Proof.Reduction]
z:81 [binder, in Proof.Application]
other
_ ⊢ _ ⇐ _ [notation, in Proof.Typing]_ ⊢ _ ⇒ _ [notation, in Proof.Typing]
_ ⟾ _ [notation, in Proof.Reduction]
_ ⊢ _ <: _ [notation, in Proof.Appsub]
_ · _ ⟹ _ [notation, in Proof.Application]
_ ⇝ [ _ ] _ [notation, in Proof.Casting]
_ ≋ _ [notation, in Proof.Subtyping.Subtyping]
_ <: _ [notation, in Proof.Subtyping.Subtyping]
_ ↩ _ ↪ _ [notation, in Proof.Subtyping.Splitable]
_ ◍ _ [notation, in Proof.Language]
_ _ . _ : _ [notation, in Proof.Language]
_ ∷ _ [notation, in Proof.Language]
_ & _ [notation, in Proof.Language]
_ → _ [notation, in Proof.Language]
appsub? _ _ [notation, in Proof.Appsub]
{ _ ↦ _ } _ [notation, in Proof.Language]
{ _ = _ } [notation, in Proof.Language]
{ _ : _ } [notation, in Proof.Language]
Notation Index
other
_ ⊢ _ ⇐ _ [in Proof.Typing]_ ⊢ _ ⇒ _ [in Proof.Typing]
_ ⟾ _ [in Proof.Reduction]
_ ⊢ _ <: _ [in Proof.Appsub]
_ · _ ⟹ _ [in Proof.Application]
_ ⇝ [ _ ] _ [in Proof.Casting]
_ ≋ _ [in Proof.Subtyping.Subtyping]
_ <: _ [in Proof.Subtyping.Subtyping]
_ ↩ _ ↪ _ [in Proof.Subtyping.Splitable]
_ ◍ _ [in Proof.Language]
_ _ . _ : _ [in Proof.Language]
_ ∷ _ [in Proof.Language]
_ & _ [in Proof.Language]
_ → _ [in Proof.Language]
appsub? _ _ [in Proof.Appsub]
{ _ ↦ _ } _ [in Proof.Language]
{ _ = _ } [in Proof.Language]
{ _ : _ } [in Proof.Language]
Binder Index
A
A1:12 [in Proof.Application]A1:17 [in Proof.Subtyping.Splitable]
A1:189 [in Proof.Appsub]
A1:20 [in Proof.Subtyping.Splitable]
A1:23 [in Proof.Subtyping.Splitable]
A1:26 [in Proof.Subtyping.Splitable]
A1:28 [in Proof.Casting]
A1:32 [in Proof.Subtyping.Splitable]
A1:36 [in Proof.Subtyping.Subtyping]
A1:39 [in Proof.Subtyping.Subtyping]
A1:42 [in Proof.Subtyping.Subtyping]
A1:46 [in Proof.Subtyping.Subtyping]
A1:59 [in Proof.Subtyping.Subtyping]
A1:75 [in Proof.Subtyping.Subtyping]
A1:81 [in Proof.Subtyping.Subtyping]
A1:9 [in Proof.Reduction]
A2:10 [in Proof.Reduction]
A2:13 [in Proof.Application]
A2:18 [in Proof.Subtyping.Splitable]
A2:190 [in Proof.Appsub]
A2:21 [in Proof.Subtyping.Splitable]
A2:24 [in Proof.Subtyping.Splitable]
A2:27 [in Proof.Subtyping.Splitable]
A2:29 [in Proof.Casting]
A2:33 [in Proof.Subtyping.Splitable]
A2:37 [in Proof.Subtyping.Subtyping]
A2:40 [in Proof.Subtyping.Subtyping]
A2:43 [in Proof.Subtyping.Subtyping]
A2:47 [in Proof.Subtyping.Subtyping]
A2:60 [in Proof.Subtyping.Subtyping]
A2:76 [in Proof.Subtyping.Subtyping]
A2:82 [in Proof.Subtyping.Subtyping]
A3:28 [in Proof.Subtyping.Splitable]
A4:29 [in Proof.Subtyping.Splitable]
A:102 [in Proof.Application]
A:106 [in Proof.Application]
A:11 [in Proof.Appsub]
A:11 [in Proof.Subtyping.Subtyping]
A:11 [in Proof.Subtyping.Splitable]
A:11 [in Proof.PrincipalTyping]
A:112 [in Proof.Application]
A:118 [in Proof.Application]
A:12 [in Proof.Typing]
A:124 [in Proof.Application]
A:128 [in Proof.Application]
A:134 [in Proof.Application]
A:137 [in Proof.Application]
A:14 [in Proof.Appsub]
A:14 [in Proof.Casting]
A:14 [in Proof.PrincipalTyping]
A:143 [in Proof.Application]
A:15 [in Proof.Value]
A:15 [in Proof.Subtyping.Subtyping]
A:16 [in Proof.Subtyping.Splitable]
A:17 [in Proof.Application]
A:17 [in Proof.PrincipalTyping]
A:18 [in Proof.Subtyping.Subtyping]
A:186 [in Proof.Appsub]
A:19 [in Proof.Typing]
A:19 [in Proof.Reduction]
A:19 [in Proof.Appsub]
A:19 [in Proof.Casting]
A:19 [in Proof.Subtyping.Splitable]
A:191 [in Proof.Appsub]
A:193 [in Proof.Appsub]
A:196 [in Proof.Appsub]
A:198 [in Proof.Appsub]
A:20 [in Proof.Appsub]
A:201 [in Proof.Appsub]
A:204 [in Proof.Appsub]
A:21 [in Proof.Typing]
A:21 [in Proof.Subtyping.Subtyping]
A:22 [in Proof.Reduction]
A:22 [in Proof.Subtyping.Splitable]
A:23 [in Proof.Appsub]
A:23 [in Proof.Casting]
A:24 [in Proof.Typing]
A:24 [in Proof.Value]
A:25 [in Proof.Appsub]
A:25 [in Proof.Subtyping.Splitable]
A:26 [in Proof.Subtyping.Subtyping]
A:27 [in Proof.Casting]
A:28 [in Proof.Application]
A:28 [in Proof.Subtyping.Subtyping]
A:29 [in Proof.Appsub]
A:29 [in Proof.Value]
A:3 [in Proof.Subtyping.Subtyping]
A:3 [in Proof.Subtyping.Splitable]
A:30 [in Proof.Subtyping.Splitable]
A:31 [in Proof.Subtyping.Subtyping]
A:31 [in Proof.Subtyping.Splitable]
A:32 [in Proof.Typing]
A:32 [in Proof.Casting]
A:33 [in Proof.Appsub]
A:34 [in Proof.Subtyping.Subtyping]
A:35 [in Proof.Typing]
A:35 [in Proof.Application]
A:35 [in Proof.Casting]
A:35 [in Proof.Subtyping.Subtyping]
A:37 [in Proof.Casting]
A:37 [in Proof.Value]
A:38 [in Proof.LocallyNameless]
A:38 [in Proof.Appsub]
A:38 [in Proof.Subtyping.Subtyping]
A:4 [in Proof.Casting]
A:4 [in Proof.Subtyping.Subtyping]
A:41 [in Proof.Typing]
A:41 [in Proof.Appsub]
A:41 [in Proof.Casting]
A:41 [in Proof.Subtyping.Subtyping]
A:42 [in Proof.Application]
A:44 [in Proof.Typing]
A:44 [in Proof.Appsub]
A:44 [in Proof.Subtyping.Subtyping]
A:45 [in Proof.Casting]
A:45 [in Proof.Value]
A:47 [in Proof.Typing]
A:48 [in Proof.Typing]
A:48 [in Proof.Reduction]
A:48 [in Proof.Appsub]
A:48 [in Proof.Subtyping.Subtyping]
A:5 [in Proof.Reduction]
A:5 [in Proof.Appsub]
A:5 [in Proof.PrincipalTyping]
A:5 [in Proof.Language]
A:51 [in Proof.Value]
A:52 [in Proof.Reduction]
A:52 [in Proof.Application]
A:54 [in Proof.Subtyping.Subtyping]
A:55 [in Proof.Reduction]
A:55 [in Proof.Appsub]
A:57 [in Proof.Subtyping.Subtyping]
A:58 [in Proof.Reduction]
A:58 [in Proof.Appsub]
A:58 [in Proof.Value]
A:58 [in Proof.Subtyping.Subtyping]
A:6 [in Proof.Appsub]
A:6 [in Proof.Application]
A:6 [in Proof.Casting]
A:6 [in Proof.Value]
A:6 [in Proof.Subtyping.Splitable]
A:60 [in Proof.Value]
A:61 [in Proof.Subtyping.Subtyping]
A:63 [in Proof.Appsub]
A:63 [in Proof.Application]
A:64 [in Proof.Subtyping.Subtyping]
A:65 [in Proof.Subtyping.Subtyping]
A:66 [in Proof.Appsub]
A:66 [in Proof.Subtyping.Subtyping]
A:68 [in Proof.Application]
A:69 [in Proof.Appsub]
A:71 [in Proof.Subtyping.Subtyping]
A:73 [in Proof.Subtyping.Subtyping]
A:74 [in Proof.Appsub]
A:77 [in Proof.Reduction]
A:78 [in Proof.Application]
A:79 [in Proof.Appsub]
A:8 [in Proof.Reduction]
A:8 [in Proof.Subtyping.Subtyping]
A:8 [in Proof.PrincipalTyping]
A:80 [in Proof.Subtyping.Subtyping]
A:83 [in Proof.Application]
A:85 [in Proof.Appsub]
A:86 [in Proof.Subtyping.Subtyping]
A:89 [in Proof.Application]
A:89 [in Proof.Subtyping.Subtyping]
A:9 [in Proof.Typing]
A:9 [in Proof.Appsub]
A:9 [in Proof.Application]
A:9 [in Proof.Subtyping.Splitable]
A:90 [in Proof.Appsub]
A:91 [in Proof.Subtyping.Subtyping]
A:93 [in Proof.Appsub]
A:93 [in Proof.Subtyping.Subtyping]
A:95 [in Proof.Subtyping.Subtyping]
A:97 [in Proof.Application]
A:97 [in Proof.Subtyping.Subtyping]
B
B1:13 [in Proof.Subtyping.Subtyping]B1:13 [in Proof.Subtyping.Splitable]
B1:45 [in Proof.Appsub]
B1:50 [in Proof.Subtyping.Subtyping]
B1:51 [in Proof.Appsub]
B1:52 [in Proof.Value]
B1:78 [in Proof.Subtyping.Subtyping]
B1:84 [in Proof.Subtyping.Subtyping]
B2:14 [in Proof.Subtyping.Subtyping]
B2:14 [in Proof.Subtyping.Splitable]
B2:46 [in Proof.Appsub]
B2:51 [in Proof.Subtyping.Subtyping]
B2:52 [in Proof.Appsub]
B2:53 [in Proof.Value]
B2:79 [in Proof.Subtyping.Subtyping]
B2:85 [in Proof.Subtyping.Subtyping]
B:10 [in Proof.Subtyping.Splitable]
B:107 [in Proof.Application]
B:114 [in Proof.Application]
B:119 [in Proof.Application]
B:12 [in Proof.Appsub]
B:12 [in Proof.Subtyping.Subtyping]
B:12 [in Proof.Subtyping.Splitable]
B:125 [in Proof.Application]
B:129 [in Proof.Application]
B:13 [in Proof.Typing]
B:138 [in Proof.Application]
B:15 [in Proof.Appsub]
B:15 [in Proof.PrincipalTyping]
B:16 [in Proof.Subtyping.Subtyping]
B:18 [in Proof.Application]
B:18 [in Proof.PrincipalTyping]
B:19 [in Proof.Subtyping.Subtyping]
B:195 [in Proof.Appsub]
B:200 [in Proof.Appsub]
B:203 [in Proof.Appsub]
B:21 [in Proof.Appsub]
B:22 [in Proof.Subtyping.Subtyping]
B:25 [in Proof.Typing]
B:25 [in Proof.Value]
B:26 [in Proof.Appsub]
B:27 [in Proof.Subtyping.Subtyping]
B:29 [in Proof.Application]
B:29 [in Proof.Subtyping.Subtyping]
B:30 [in Proof.Appsub]
B:32 [in Proof.Subtyping.Subtyping]
B:33 [in Proof.Typing]
B:34 [in Proof.Appsub]
B:36 [in Proof.Typing]
B:36 [in Proof.Application]
B:38 [in Proof.Casting]
B:39 [in Proof.LocallyNameless]
B:39 [in Proof.Appsub]
B:4 [in Proof.Subtyping.Splitable]
B:42 [in Proof.Typing]
B:42 [in Proof.Appsub]
B:43 [in Proof.Application]
B:45 [in Proof.Subtyping.Subtyping]
B:46 [in Proof.Casting]
B:49 [in Proof.Typing]
B:49 [in Proof.Reduction]
B:49 [in Proof.Appsub]
B:49 [in Proof.Subtyping.Subtyping]
B:5 [in Proof.Subtyping.Subtyping]
B:55 [in Proof.Subtyping.Subtyping]
B:56 [in Proof.Appsub]
B:59 [in Proof.Appsub]
B:6 [in Proof.Reduction]
B:6 [in Proof.PrincipalTyping]
B:61 [in Proof.Value]
B:62 [in Proof.Subtyping.Subtyping]
B:64 [in Proof.Appsub]
B:67 [in Proof.Subtyping.Subtyping]
B:7 [in Proof.Appsub]
B:7 [in Proof.Casting]
B:7 [in Proof.Value]
B:70 [in Proof.Appsub]
B:74 [in Proof.Subtyping.Subtyping]
B:75 [in Proof.Appsub]
B:77 [in Proof.Subtyping.Subtyping]
B:80 [in Proof.Appsub]
B:83 [in Proof.Subtyping.Subtyping]
B:86 [in Proof.Appsub]
B:87 [in Proof.Subtyping.Subtyping]
B:9 [in Proof.Subtyping.Subtyping]
B:90 [in Proof.Application]
B:90 [in Proof.Subtyping.Subtyping]
B:91 [in Proof.Appsub]
B:92 [in Proof.Subtyping.Subtyping]
B:94 [in Proof.Subtyping.Subtyping]
B:96 [in Proof.Subtyping.Subtyping]
B:98 [in Proof.Application]
B:98 [in Proof.Subtyping.Subtyping]
C
C1:36 [in Proof.Appsub]C1:53 [in Proof.Appsub]
C2:37 [in Proof.Appsub]
C2:54 [in Proof.Appsub]
C:108 [in Proof.Application]
C:120 [in Proof.Application]
C:130 [in Proof.Application]
C:17 [in Proof.Subtyping.Subtyping]
C:19 [in Proof.Application]
C:20 [in Proof.Subtyping.Subtyping]
C:22 [in Proof.Appsub]
C:23 [in Proof.Subtyping.Subtyping]
C:26 [in Proof.Typing]
C:28 [in Proof.Appsub]
C:30 [in Proof.Subtyping.Subtyping]
C:32 [in Proof.Appsub]
C:33 [in Proof.Subtyping.Subtyping]
C:47 [in Proof.Casting]
C:50 [in Proof.Appsub]
C:6 [in Proof.Subtyping.Subtyping]
C:60 [in Proof.Appsub]
C:68 [in Proof.Subtyping.Subtyping]
C:71 [in Proof.Appsub]
C:78 [in Proof.Appsub]
C:8 [in Proof.Appsub]
C:8 [in Proof.Casting]
C:81 [in Proof.Appsub]
C:88 [in Proof.Subtyping.Subtyping]
C:89 [in Proof.Appsub]
C:91 [in Proof.Application]
D
dir:56 [in Proof.Reduction]dir:59 [in Proof.Reduction]
dir:64 [in Proof.Application]
dir:69 [in Proof.Application]
dir:78 [in Proof.Reduction]
dir:79 [in Proof.Application]
dir:92 [in Proof.Application]
D:109 [in Proof.Application]
D:20 [in Proof.Application]
D:24 [in Proof.Subtyping.Subtyping]
D:62 [in Proof.Appsub]
D:7 [in Proof.Subtyping.Subtyping]
D:73 [in Proof.Appsub]
D:84 [in Proof.Appsub]
D:9 [in Proof.Casting]
D:93 [in Proof.Application]
E
e':21 [in Proof.Reduction]e':31 [in Proof.Reduction]
e':33 [in Proof.Reduction]
e':44 [in Proof.Reduction]
e':47 [in Proof.Reduction]
e':51 [in Proof.Reduction]
e':54 [in Proof.Reduction]
e':60 [in Proof.Reduction]
e':73 [in Proof.Reduction]
e':76 [in Proof.Reduction]
e1':24 [in Proof.Reduction]
e1':36 [in Proof.Reduction]
e1:10 [in Proof.Application]
e1:10 [in Proof.Value]
e1:12 [in Proof.Value]
e1:12 [in Proof.PrincipalTyping]
e1:17 [in Proof.LocallyNameless]
e1:23 [in Proof.Reduction]
e1:27 [in Proof.Typing]
e1:35 [in Proof.Reduction]
e1:37 [in Proof.Typing]
e1:40 [in Proof.LocallyNameless]
e1:46 [in Proof.Application]
e1:46 [in Proof.Value]
e1:48 [in Proof.Value]
e1:73 [in Proof.Application]
e2':28 [in Proof.Reduction]
e2':40 [in Proof.Reduction]
e2:11 [in Proof.Application]
e2:11 [in Proof.Value]
e2:13 [in Proof.Value]
e2:13 [in Proof.PrincipalTyping]
e2:18 [in Proof.LocallyNameless]
e2:25 [in Proof.Reduction]
e2:27 [in Proof.Reduction]
e2:28 [in Proof.Typing]
e2:37 [in Proof.Reduction]
e2:38 [in Proof.Typing]
e2:39 [in Proof.Reduction]
e2:41 [in Proof.LocallyNameless]
e2:47 [in Proof.Application]
e2:47 [in Proof.Value]
e2:49 [in Proof.Value]
e2:74 [in Proof.Application]
E:10 [in Proof.Casting]
e:10 [in Proof.PrincipalTyping]
e:101 [in Proof.Application]
e:105 [in Proof.Application]
e:11 [in Proof.Casting]
e:113 [in Proof.Application]
e:117 [in Proof.Application]
e:123 [in Proof.Application]
e:13 [in Proof.Reduction]
e:131 [in Proof.Application]
e:135 [in Proof.Application]
e:14 [in Proof.Typing]
e:14 [in Proof.Value]
e:14 [in Proof.Language]
e:140 [in Proof.Application]
e:144 [in Proof.Application]
e:16 [in Proof.Reduction]
e:16 [in Proof.LocallyNameless]
e:16 [in Proof.Value]
e:16 [in Proof.PrincipalTyping]
e:17 [in Proof.Typing]
e:17 [in Proof.Language]
e:18 [in Proof.Value]
e:2 [in Proof.LocallyNameless]
e:20 [in Proof.Reduction]
e:22 [in Proof.Typing]
e:22 [in Proof.Language]
e:23 [in Proof.Application]
e:23 [in Proof.Value]
e:25 [in Proof.LocallyNameless]
e:25 [in Proof.Language]
e:28 [in Proof.LocallyNameless]
e:28 [in Proof.Value]
e:30 [in Proof.Typing]
e:30 [in Proof.Reduction]
e:31 [in Proof.LocallyNameless]
e:32 [in Proof.Reduction]
e:32 [in Proof.Application]
e:35 [in Proof.LocallyNameless]
e:36 [in Proof.LocallyNameless]
e:36 [in Proof.Value]
e:39 [in Proof.Application]
e:4 [in Proof.Reduction]
e:4 [in Proof.PrincipalTyping]
e:40 [in Proof.Typing]
e:42 [in Proof.Reduction]
e:43 [in Proof.Reduction]
e:44 [in Proof.Value]
e:46 [in Proof.Typing]
e:46 [in Proof.Reduction]
e:5 [in Proof.Application]
e:5 [in Proof.Value]
e:50 [in Proof.Typing]
e:50 [in Proof.Reduction]
e:50 [in Proof.Value]
e:53 [in Proof.Reduction]
e:55 [in Proof.Application]
e:55 [in Proof.Value]
e:56 [in Proof.Value]
e:57 [in Proof.Reduction]
e:58 [in Proof.Application]
e:59 [in Proof.Value]
E:60 [in Proof.Application]
e:62 [in Proof.Application]
E:65 [in Proof.Application]
e:67 [in Proof.Application]
e:7 [in Proof.Application]
e:7 [in Proof.PrincipalTyping]
E:70 [in Proof.Application]
e:71 [in Proof.Application]
e:72 [in Proof.Reduction]
e:74 [in Proof.Reduction]
e:75 [in Proof.Reduction]
e:75 [in Proof.Value]
e:76 [in Proof.Value]
e:77 [in Proof.Application]
e:8 [in Proof.Language]
e:80 [in Proof.Application]
E:85 [in Proof.Application]
e:88 [in Proof.Application]
e:9 [in Proof.LocallyNameless]
e:96 [in Proof.Application]
F
f:11 [in Proof.Reduction]f:126 [in Proof.Application]
F:61 [in Proof.Application]
F:66 [in Proof.Application]
F:84 [in Proof.Application]
G
G:59 [in Proof.Application]H
H1:82 [in Proof.Appsub]H2:83 [in Proof.Appsub]
H:57 [in Proof.Appsub]
H:61 [in Proof.Appsub]
H:65 [in Proof.Appsub]
H:68 [in Proof.Appsub]
H:72 [in Proof.Appsub]
H:76 [in Proof.Appsub]
H:87 [in Proof.Appsub]
I
i:11 [in Proof.Language]i:12 [in Proof.LocallyNameless]
i:45 [in Proof.Reduction]
J
j:10 [in Proof.LocallyNameless]K
k:14 [in Proof.LocallyNameless]k:20 [in Proof.Language]
k:21 [in Proof.LocallyNameless]
k:42 [in Proof.LocallyNameless]
k:75 [in Proof.Application]
L
L:10 [in Proof.Typing]l:10 [in Proof.Appsub]
l:10 [in Proof.Subtyping.Subtyping]
l:100 [in Proof.Application]
l:116 [in Proof.Application]
l:121 [in Proof.Application]
l:139 [in Proof.Application]
l:14 [in Proof.Reduction]
l:14 [in Proof.Application]
l:142 [in Proof.Application]
l:15 [in Proof.Casting]
l:15 [in Proof.Subtyping.Splitable]
l:17 [in Proof.Value]
l:18 [in Proof.Typing]
l:19 [in Proof.Value]
l:24 [in Proof.Appsub]
l:25 [in Proof.Application]
l:25 [in Proof.Subtyping.Subtyping]
l:29 [in Proof.Reduction]
l:30 [in Proof.Value]
l:31 [in Proof.Typing]
l:34 [in Proof.Reduction]
l:38 [in Proof.Value]
l:5 [in Proof.Subtyping.Splitable]
l:54 [in Proof.Value]
l:56 [in Proof.Subtyping.Subtyping]
l:62 [in Proof.Value]
l:63 [in Proof.Subtyping.Subtyping]
l:67 [in Proof.Appsub]
l:68 [in Proof.Value]
l:72 [in Proof.Subtyping.Subtyping]
l:77 [in Proof.Appsub]
l:8 [in Proof.Application]
L:8 [in Proof.Value]
l:88 [in Proof.Appsub]
l:9 [in Proof.PrincipalTyping]
N
n:22 [in Proof.Value]n:3 [in Proof.Reduction]
n:3 [in Proof.Casting]
n:3 [in Proof.Value]
n:3 [in Proof.PrincipalTyping]
n:6 [in Proof.Typing]
P
P:1 [in Proof.Tactical]p:42 [in Proof.Value]
p:7 [in Proof.Reduction]
Q
Q:2 [in Proof.Tactical]R
R:63 [in Proof.Reduction]R:71 [in Proof.Reduction]
S
S:13 [in Proof.Appsub]S:16 [in Proof.Appsub]
S:187 [in Proof.Appsub]
S:188 [in Proof.Appsub]
S:192 [in Proof.Appsub]
S:194 [in Proof.Appsub]
S:197 [in Proof.Appsub]
S:199 [in Proof.Appsub]
S:202 [in Proof.Appsub]
S:205 [in Proof.Appsub]
S:27 [in Proof.Appsub]
S:31 [in Proof.Appsub]
S:35 [in Proof.Appsub]
S:40 [in Proof.Appsub]
S:43 [in Proof.Appsub]
S:47 [in Proof.Appsub]
S:94 [in Proof.Appsub]
T
TA1:49 [in Proof.Application]TA2:50 [in Proof.Application]
TA:31 [in Proof.Application]
TA:38 [in Proof.Application]
TA:45 [in Proof.Application]
T1:44 [in Proof.LocallyNameless]
T2:45 [in Proof.LocallyNameless]
T:11 [in Proof.Typing]
T:16 [in Proof.Typing]
T:20 [in Proof.Typing]
T:23 [in Proof.Typing]
T:29 [in Proof.Typing]
T:34 [in Proof.Typing]
T:39 [in Proof.Typing]
T:45 [in Proof.Typing]
T:5 [in Proof.Typing]
T:51 [in Proof.Typing]
T:7 [in Proof.Typing]
T:72 [in Proof.Application]
T:76 [in Proof.Application]
U
u1:32 [in Proof.Value]u1:70 [in Proof.Value]
u1:72 [in Proof.Value]
u2:33 [in Proof.Value]
u2:71 [in Proof.Value]
u2:73 [in Proof.Value]
u:13 [in Proof.LocallyNameless]
u:13 [in Proof.Language]
u:15 [in Proof.LocallyNameless]
u:19 [in Proof.LocallyNameless]
u:21 [in Proof.Language]
u:24 [in Proof.LocallyNameless]
u:26 [in Proof.Language]
u:27 [in Proof.LocallyNameless]
u:3 [in Proof.LocallyNameless]
u:30 [in Proof.LocallyNameless]
u:31 [in Proof.Value]
u:34 [in Proof.LocallyNameless]
u:37 [in Proof.LocallyNameless]
u:43 [in Proof.Typing]
u:5 [in Proof.LocallyNameless]
u:69 [in Proof.Value]
u:8 [in Proof.LocallyNameless]
u:82 [in Proof.Application]
V
vl:104 [in Proof.Application]vl:30 [in Proof.Application]
vl:37 [in Proof.Application]
vl:44 [in Proof.Application]
vl:48 [in Proof.Application]
vl:54 [in Proof.Application]
vl:57 [in Proof.Application]
vl:95 [in Proof.Application]
v':13 [in Proof.Casting]
v':18 [in Proof.Reduction]
v':22 [in Proof.Application]
v':31 [in Proof.Casting]
v':34 [in Proof.Casting]
v':39 [in Proof.Casting]
v':42 [in Proof.Casting]
v':44 [in Proof.Casting]
v1:110 [in Proof.Application]
v1:132 [in Proof.Application]
v1:16 [in Proof.Casting]
v1:20 [in Proof.Casting]
v1:24 [in Proof.Casting]
v1:26 [in Proof.Application]
v1:33 [in Proof.Application]
v1:40 [in Proof.Application]
v1:40 [in Proof.Value]
v1:64 [in Proof.Value]
v1:66 [in Proof.Value]
v2:111 [in Proof.Application]
v2:133 [in Proof.Application]
v2:17 [in Proof.Casting]
v2:21 [in Proof.Casting]
v2:25 [in Proof.Casting]
v2:27 [in Proof.Application]
v2:34 [in Proof.Application]
v2:41 [in Proof.Application]
v2:41 [in Proof.Value]
v2:65 [in Proof.Value]
v2:67 [in Proof.Value]
v:103 [in Proof.Application]
v:11 [in Proof.LocallyNameless]
v:115 [in Proof.Application]
v:12 [in Proof.Reduction]
v:12 [in Proof.Casting]
v:122 [in Proof.Application]
v:127 [in Proof.Application]
v:136 [in Proof.Application]
v:141 [in Proof.Application]
v:15 [in Proof.Reduction]
v:17 [in Proof.Reduction]
v:18 [in Proof.Casting]
v:21 [in Proof.Application]
v:22 [in Proof.Casting]
v:24 [in Proof.Application]
v:26 [in Proof.Reduction]
v:26 [in Proof.Casting]
v:30 [in Proof.Casting]
v:33 [in Proof.Casting]
v:36 [in Proof.Casting]
v:38 [in Proof.Reduction]
v:39 [in Proof.Value]
v:40 [in Proof.Casting]
v:41 [in Proof.Reduction]
v:43 [in Proof.Casting]
v:43 [in Proof.Value]
v:5 [in Proof.Casting]
v:51 [in Proof.Application]
v:53 [in Proof.Application]
v:56 [in Proof.Application]
v:57 [in Proof.Value]
v:63 [in Proof.Value]
v:74 [in Proof.Value]
v:87 [in Proof.Application]
v:94 [in Proof.Application]
v:99 [in Proof.Application]
X
x:1 [in Proof.LocallyNameless]x:15 [in Proof.Typing]
x:20 [in Proof.LocallyNameless]
x:22 [in Proof.LocallyNameless]
x:26 [in Proof.LocallyNameless]
x:27 [in Proof.Language]
x:28 [in Proof.Language]
x:29 [in Proof.LocallyNameless]
x:29 [in Proof.Language]
x:30 [in Proof.Language]
x:32 [in Proof.LocallyNameless]
x:4 [in Proof.LocallyNameless]
x:4 [in Proof.Value]
x:43 [in Proof.LocallyNameless]
x:6 [in Proof.LocallyNameless]
X:61 [in Proof.Reduction]
X:62 [in Proof.Reduction]
x:66 [in Proof.Reduction]
x:67 [in Proof.Reduction]
X:70 [in Proof.Reduction]
x:8 [in Proof.Typing]
x:86 [in Proof.Application]
x:9 [in Proof.Value]
Y
y:23 [in Proof.LocallyNameless]y:33 [in Proof.LocallyNameless]
y:68 [in Proof.Reduction]
y:7 [in Proof.LocallyNameless]
Z
z:12 [in Proof.Language]z:69 [in Proof.Reduction]
z:81 [in Proof.Application]
Library Index
A
ApplicationAppsub
C
CastingL
LanguageLocallyNameless
P
PrincipalTypingR
ReductionS
SplitableSubtyping
T
TacticalTyping
V
ValueLemma Index
A
add_notin_context [in Proof.LocallyNameless]appsub_iso_l [in Proof.Appsub]
appsub_iso_v [in Proof.Appsub]
appsub_iso_l2 [in Proof.Appsub]
appsub_iso_v2 [in Proof.Appsub]
appsub_iso_v1 [in Proof.Appsub]
appsub_split_inversion [in Proof.Appsub]
appsub_determinism [in Proof.Appsub]
appsub_to_auxas [in Proof.Appsub]
atype_determinism [in Proof.Application]
auxas_not_and [in Proof.Appsub]
auxas_iso_l2 [in Proof.Appsub]
auxas_iso_v2 [in Proof.Appsub]
auxas_iso_v1 [in Proof.Appsub]
auxas_false [in Proof.Appsub]
C
casting_preservation [in Proof.Casting]casting_progress [in Proof.Casting]
casting_progress' [in Proof.Casting]
casting_value [in Proof.Casting]
casting_lc [in Proof.Casting]
F
fv_open_lower [in Proof.LocallyNameless]fv_in_dom [in Proof.Application]
fv_open_lower [in Proof.Application]
I
isosub_to_sub2 [in Proof.Subtyping.Subtyping]isosub_to_sub1 [in Proof.Subtyping.Subtyping]
isosub_sound [in Proof.Subtyping.Subtyping]
isosub_transitivity [in Proof.Subtyping.Subtyping]
isosub_inv_splitable [in Proof.Subtyping.Subtyping]
L
lc_inv_rcd [in Proof.Value]lc_inv_lam [in Proof.Value]
lc_inv_merge_r [in Proof.Value]
lc_inv_merge_l [in Proof.Value]
lc_inv_anno [in Proof.Value]
lc_value [in Proof.Value]
lc_pvalue [in Proof.Value]
M
modusponens [in Proof.Tactical]O
open_abs [in Proof.LocallyNameless]open_rec_lc [in Proof.LocallyNameless]
open_rec_lc_core [in Proof.LocallyNameless]
ordinary_decidable [in Proof.Subtyping.Splitable]
P
papp_progress_l_formal [in Proof.Application]papp_progress_l [in Proof.Application]
papp_progress_v_formal [in Proof.Application]
papp_progress_v [in Proof.Application]
papp_preservation_l_formal [in Proof.Application]
papp_preservation_l [in Proof.Application]
papp_preservation_v_formal [in Proof.Application]
papp_preservation_v [in Proof.Application]
papp_uvalue_l [in Proof.Application]
papp_uvalue_v [in Proof.Application]
papp_lc_l [in Proof.Application]
papp_lc_v [in Proof.Application]
preservation [in Proof.Reduction]
preservation_gen [in Proof.Reduction]
preservation_chk [in Proof.Reduction]
progress [in Proof.Reduction]
proper_complete [in Proof.Subtyping.Subtyping]
proper_record [in Proof.Subtyping.Subtyping]
proper_arrow [in Proof.Subtyping.Subtyping]
psub_auxas_false [in Proof.Appsub]
psub_appsub_false [in Proof.Appsub]
psub_complete_appsub [in Proof.Appsub]
psub_sound_auxas [in Proof.Appsub]
psub_sound_appsub [in Proof.Appsub]
psub_none_auxas2 [in Proof.Appsub]
psub_none_auxas1 [in Proof.Appsub]
ptype_determinism [in Proof.PrincipalTyping]
pvalue_decidable [in Proof.Value]
pvalue_and_value [in Proof.Value]
S
soundness [in Proof.Reduction]splitable_decrease_size [in Proof.Subtyping.Splitable]
splitable_determinism [in Proof.Subtyping.Splitable]
splitable_or_ordinary [in Proof.Subtyping.Splitable]
splitable_not_ordinary [in Proof.Subtyping.Splitable]
step_lc [in Proof.Reduction]
substitution_lemma [in Proof.Application]
subst_notin_fv [in Proof.LocallyNameless]
subst_intro [in Proof.LocallyNameless]
subst_lc [in Proof.LocallyNameless]
subst_open_var [in Proof.LocallyNameless]
subst_open_rec [in Proof.LocallyNameless]
subst_neq_var [in Proof.LocallyNameless]
subst_eq_var [in Proof.LocallyNameless]
subst_fresh [in Proof.LocallyNameless]
subst_value [in Proof.Application]
sub_arrow_int [in Proof.Subtyping.Subtyping]
sub_transitivity [in Proof.Subtyping.Subtyping]
sub_inv_splitable_r [in Proof.Subtyping.Subtyping]
sub_inv_splitable_l [in Proof.Subtyping.Subtyping]
sub_splitable [in Proof.Subtyping.Subtyping]
sub_splitable_r [in Proof.Subtyping.Subtyping]
sub_splitable_l [in Proof.Subtyping.Subtyping]
sub_reflexivity [in Proof.Subtyping.Subtyping]
sub_and_r [in Proof.Subtyping.Subtyping]
sub_and_l [in Proof.Subtyping.Subtyping]
sub_record [in Proof.Subtyping.Subtyping]
sub_arrow [in Proof.Subtyping.Subtyping]
T
typing_chk_sub [in Proof.Typing]typing_to_lc [in Proof.Typing]
typing_to_ptype [in Proof.Typing]
typing_uniq [in Proof.Application]
typing_weakening [in Proof.Application]
typing_weakening_gen [in Proof.Application]
typing_to_atype [in Proof.Application]
U
uvalue_inv_merge_r [in Proof.Value]uvalue_inv_merge_l [in Proof.Value]
uvalue_inv_rcd [in Proof.Value]
V
value_no_step [in Proof.Reduction]value_decidable [in Proof.Value]
value_is_uvalue [in Proof.Value]
value_inv_merge_r [in Proof.Value]
value_inv_merge_l [in Proof.Value]
value_inv_rcd [in Proof.Value]
value_anno_ordinary [in Proof.Value]
value_and_value_anno [in Proof.Value]
Constructor Index
A
Aas_And_R [in Proof.Appsub]Aas_And_L [in Proof.Appsub]
Aas_Lbl [in Proof.Appsub]
Aas_Arr [in Proof.Appsub]
Aas_Refl [in Proof.Appsub]
Al [in Proof.Application]
Alt [in Proof.Appsub]
And [in Proof.Language]
Ann [in Proof.Language]
App [in Proof.Language]
Arr [in Proof.Language]
As_And_P [in Proof.Appsub]
As_And_R [in Proof.Appsub]
As_And_L [in Proof.Appsub]
As_Lbl [in Proof.Appsub]
As_Arr [in Proof.Appsub]
As_Refl [in Proof.Appsub]
At_Lbl [in Proof.Application]
At_Mrg [in Proof.Application]
At_Rcd [in Proof.Application]
At_Ann [in Proof.Application]
Av [in Proof.Application]
Avt [in Proof.Appsub]
B
Bvar [in Proof.Language]C
Chk [in Proof.Typing]Ct_And [in Proof.Casting]
Ct_Mrg_R [in Proof.Casting]
Ct_Mrg_L [in Proof.Casting]
Ct_Rcd [in Proof.Casting]
Ct_Lam [in Proof.Casting]
Ct_Top [in Proof.Casting]
Ct_Lit [in Proof.Casting]
F
Fld [in Proof.Language]Fvar [in Proof.Language]
I
Inf [in Proof.Typing]Int [in Proof.Language]
Isub_And [in Proof.Subtyping.Subtyping]
Isub_Rcd [in Proof.Subtyping.Subtyping]
Isub_Refl [in Proof.Subtyping.Subtyping]
L
Lam [in Proof.Language]Lc_Prj [in Proof.Value]
Lc_Fld [in Proof.Value]
Lc_Ann [in Proof.Value]
Lc_Mrg [in Proof.Value]
Lc_App [in Proof.Value]
Lc_Lam [in Proof.Value]
Lc_Var [in Proof.Value]
Lc_Lit [in Proof.Value]
Lit [in Proof.Language]
M
Mrg [in Proof.Language]multi_step [in Proof.Reduction]
multi_refl [in Proof.Reduction]
O
Ord_Rcd [in Proof.Subtyping.Splitable]Ord_Arr [in Proof.Subtyping.Splitable]
Ord_Tnt [in Proof.Subtyping.Splitable]
Ord_Top [in Proof.Subtyping.Splitable]
P
Pa_Mrg_P [in Proof.Application]Pa_Mrg_R [in Proof.Application]
Pa_Mrg_L [in Proof.Application]
Pa_Rcd [in Proof.Application]
Pa_Lam [in Proof.Application]
Prj [in Proof.Language]
Pr_Spl [in Proof.Subtyping.Subtyping]
Pr_Rcd [in Proof.Subtyping.Subtyping]
Pr_Arr [in Proof.Subtyping.Subtyping]
Pr_Top [in Proof.Subtyping.Subtyping]
Pr_Int [in Proof.Subtyping.Subtyping]
Pt_Mrg [in Proof.PrincipalTyping]
Pt_Rcd [in Proof.PrincipalTyping]
Pt_Ann [in Proof.PrincipalTyping]
Pt_Arr [in Proof.PrincipalTyping]
Pt_Int [in Proof.PrincipalTyping]
Pv_Lam [in Proof.Value]
Pv_Lit [in Proof.Value]
R
Rcd [in Proof.Language]S
Spl_Rcd [in Proof.Subtyping.Splitable]Spl_Arr [in Proof.Subtyping.Splitable]
Spl_And [in Proof.Subtyping.Splitable]
St_Mrg_R [in Proof.Reduction]
St_Mrg_L [in Proof.Reduction]
St_Prj_L [in Proof.Reduction]
St_Rcd [in Proof.Reduction]
St_App_R [in Proof.Reduction]
St_App_L [in Proof.Reduction]
St_Ann [in Proof.Reduction]
St_Val [in Proof.Reduction]
St_Prj [in Proof.Reduction]
St_App [in Proof.Reduction]
St_Spl [in Proof.Reduction]
St_Lam [in Proof.Reduction]
St_Lit [in Proof.Reduction]
Sub_And_R [in Proof.Subtyping.Subtyping]
Sub_And_L [in Proof.Subtyping.Subtyping]
Sub_And [in Proof.Subtyping.Subtyping]
Sub_Rcd [in Proof.Subtyping.Subtyping]
Sub_Arr [in Proof.Subtyping.Subtyping]
Sub_Top [in Proof.Subtyping.Subtyping]
Sub_Int [in Proof.Subtyping.Subtyping]
T
Top [in Proof.Language]Ty_Sub [in Proof.Typing]
Ty_Mrg [in Proof.Typing]
Ty_Prj [in Proof.Typing]
Ty_App [in Proof.Typing]
Ty_Ann [in Proof.Typing]
Ty_Rcd [in Proof.Typing]
Ty_Lam [in Proof.Typing]
Ty_Var [in Proof.Typing]
Ty_Int [in Proof.Typing]
U
Uv_Mrg [in Proof.Value]Uv_Rcd [in Proof.Value]
Uv_Ann [in Proof.Value]
V
V_Mrg [in Proof.Value]V_Rcd [in Proof.Value]
V_Ann [in Proof.Value]
Axiom Index
D
dec_sub [in Proof.Appsub]Inductive Index
A
appsub [in Proof.Appsub]arg [in Proof.Appsub]
atype [in Proof.Application]
auxas [in Proof.Appsub]
C
casting [in Proof.Casting]I
isosub [in Proof.Subtyping.Subtyping]L
lc [in Proof.Value]M
mode [in Proof.Typing]multi [in Proof.Reduction]
O
ordinary [in Proof.Subtyping.Splitable]P
papp [in Proof.Application]proper [in Proof.Subtyping.Subtyping]
ptype [in Proof.PrincipalTyping]
pvalue [in Proof.Value]
S
splitable [in Proof.Subtyping.Splitable]step [in Proof.Reduction]
sub [in Proof.Subtyping.Subtyping]
T
term [in Proof.Language]type [in Proof.Language]
typing [in Proof.Typing]
U
uvalue [in Proof.Value]V
value [in Proof.Value]vl [in Proof.Application]
Section Index
P
papp_preservation [in Proof.Application]Abbreviation Index
M
multistep [in Proof.Reduction]Definition Index
C
ctx [in Proof.Language]F
fv [in Proof.Language]I
isomorphic_spec [in Proof.Subtyping.Subtyping]L
label [in Proof.Language]N
normal_form [in Proof.Reduction]O
open [in Proof.Language]open_rec [in Proof.Language]
P
psub [in Proof.Appsub]R
relation [in Proof.Reduction]S
size_term [in Proof.Language]size_type [in Proof.Language]
stuck [in Proof.Reduction]
substitution [in Proof.Language]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (977 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (679 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (115 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (114 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |