OAI/Computability/TypeSystem/Relational.lean

GitHub source file

237 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PureTypeSystem.Labelled.RelationalCode line 13

   Source documentation

   Fixed syntax shared by both source logical channels and the A-independent probe type. The raw path is literally shared, not an isomorphism hypothesis.

   structure RelationalCode (S : Type u) where
   …

2. def OAI.PureTypeSystem.Labelled.RelationalCode.rename line 19
3. def OAI.PureTypeSystem.Labelled.RelationalCode.subst line 21
4. def OAI.PureTypeSystem.Labelled.RelationalCode.channel line 23
5. def OAI.PureTypeSystem.Labelled.RelationalCode.baseType line 24
6. def OAI.PureTypeSystem.Labelled.RelationalCode.queryBody line 25
7. def OAI.PureTypeSystem.Labelled.RelationalCode.goodBody line 27
8. def OAI.PureTypeSystem.Labelled.RelationalCode.pair line 29
9. def OAI.PureTypeSystem.Labelled.RelationalCode.rawTop line 33

   Source documentation

   The source's fixed c_top in the raw wrapper, used only by the markers.

   def rawTop (L : LogicCode S) (A : Expr S) :=
   …

   Mentions: OAI.PureTypeSystem.Labelled.Expr

10. def OAI.PureTypeSystem.Labelled.RelationalCode.point line 35
11. def OAI.PureTypeSystem.Labelled.RelationalCode.bundle line 38
12. def OAI.PureTypeSystem.Labelled.RelationalCode.diamond line 41
13. def OAI.PureTypeSystem.Labelled.RelationalCode.partBody line 43
14. def OAI.PureTypeSystem.Labelled.RelationalCode.part line 46
15. def OAI.PureTypeSystem.Labelled.RelationalCode.sb line 48
16. def OAI.PureTypeSystem.Labelled.RelationalCode.liftBody line 51
17. def OAI.PureTypeSystem.Labelled.RelationalCode.lift line 54
18. structure OAI.PureTypeSystem.Labelled.RelationalCode.Formed line 59
19. def OAI.PureTypeSystem.Labelled.ChannelSetup.relational line 67
20. theorem OAI.PureTypeSystem.Labelled.ChannelSetup.relational_formed line 69
21. theorem OAI.PureTypeSystem.Labelled.ProbeCode.rename_comp line 80
22. theorem OAI.PureTypeSystem.Labelled.ProbeCode.subst_rename line 82
23. theorem OAI.PureTypeSystem.Labelled.ProbeCode.rename_subst line 85
24. theorem OAI.PureTypeSystem.Labelled.ProbeCode.carrier_rename line 88
25. theorem OAI.PureTypeSystem.Labelled.ProbeCode.carrier_subst line 93
26. theorem OAI.PureTypeSystem.Labelled.ProbeCode.readBody_rename line 100
27. theorem OAI.PureTypeSystem.Labelled.ProbeCode.readBody_subst line 105
28. theorem OAI.PureTypeSystem.Labelled.ProbeCode.observe_rename line 110
29. theorem OAI.PureTypeSystem.Labelled.ProbeCode.observe_subst line 114
30. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decodeMap_rename line 121
31. theorem OAI.PureTypeSystem.Labelled.DoubleCode.markBody_rename line 126
32. theorem OAI.PureTypeSystem.Labelled.DoubleCode.pointBody_rename line 130
33. theorem OAI.PureTypeSystem.Labelled.DoubleCode.point_rename line 136
34. theorem OAI.PureTypeSystem.Labelled.DoubleCode.dummy_rename line 141
35. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bundle_rename line 146
36. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decodeMap_subst line 152
37. theorem OAI.PureTypeSystem.Labelled.DoubleCode.markBody_subst line 157
38. theorem OAI.PureTypeSystem.Labelled.DoubleCode.pointBody_subst line 161
39. theorem OAI.PureTypeSystem.Labelled.DoubleCode.point_subst line 167
40. theorem OAI.PureTypeSystem.Labelled.DoubleCode.dummy_subst line 172
41. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bundle_subst line 177
42. theorem OAI.PureTypeSystem.Labelled.ChannelCode.subst_rename line 187
43. theorem OAI.PureTypeSystem.Labelled.ChannelCode.rename_subst line 190
44. theorem OAI.PureTypeSystem.Labelled.ChannelCode.goodBody_subst line 193
45. theorem OAI.PureTypeSystem.Labelled.RelationalCode.rename_comp line 204
46. theorem OAI.PureTypeSystem.Labelled.RelationalCode.subst_rename line 206
47. theorem OAI.PureTypeSystem.Labelled.RelationalCode.rename_subst line 209
48. theorem OAI.PureTypeSystem.Labelled.RelationalCode.instantiate_raise line 212
49. theorem OAI.PureTypeSystem.Labelled.RelationalCode.channel_rename line 214
50. theorem OAI.PureTypeSystem.Labelled.RelationalCode.baseType_rename line 215
51. theorem OAI.PureTypeSystem.Labelled.RelationalCode.queryBody_rename line 218
52. theorem OAI.PureTypeSystem.Labelled.RelationalCode.goodBody_rename line 222
53. theorem OAI.PureTypeSystem.Labelled.RelationalCode.pair_rename line 225
54. theorem OAI.PureTypeSystem.Labelled.RelationalCode.rawTop_rename line 228
55. theorem OAI.PureTypeSystem.Labelled.RelationalCode.point_rename line 232
56. theorem OAI.PureTypeSystem.Labelled.RelationalCode.bundle_rename line 236
57. theorem OAI.PureTypeSystem.Labelled.RelationalCode.diamond_rename line 240
58. theorem OAI.PureTypeSystem.Labelled.RelationalCode.partBody_rename line 243
59. theorem OAI.PureTypeSystem.Labelled.RelationalCode.part_rename line 247
60. theorem OAI.PureTypeSystem.Labelled.RelationalCode.sb_rename line 250
61. theorem OAI.PureTypeSystem.Labelled.RelationalCode.liftBody_rename line 256
62. theorem OAI.PureTypeSystem.Labelled.RelationalCode.lift_rename line 262
63. theorem OAI.PureTypeSystem.Labelled.RelationalCode.channel_subst line 267
64. theorem OAI.PureTypeSystem.Labelled.RelationalCode.baseType_subst line 268
65. theorem OAI.PureTypeSystem.Labelled.RelationalCode.queryBody_subst line 271
66. theorem OAI.PureTypeSystem.Labelled.RelationalCode.goodBody_subst line 275
67. theorem OAI.PureTypeSystem.Labelled.RelationalCode.pair_subst line 278
68. theorem OAI.PureTypeSystem.Labelled.RelationalCode.rawTop_subst line 281
69. theorem OAI.PureTypeSystem.Labelled.RelationalCode.point_subst line 285
70. theorem OAI.PureTypeSystem.Labelled.RelationalCode.bundle_subst line 289
71. theorem OAI.PureTypeSystem.Labelled.RelationalCode.diamond_subst line 293
72. theorem OAI.PureTypeSystem.Labelled.RelationalCode.partBody_subst line 296
73. theorem OAI.PureTypeSystem.Labelled.RelationalCode.part_subst line 300
74. theorem OAI.PureTypeSystem.Labelled.RelationalCode.sb_subst line 303
75. theorem OAI.PureTypeSystem.Labelled.RelationalCode.liftBody_subst line 309
76. theorem OAI.PureTypeSystem.Labelled.RelationalCode.lift_subst line 315
77. theorem OAI.PureTypeSystem.Labelled.RelationalCode.partBody_instantiate line 320
78. theorem OAI.PureTypeSystem.Labelled.RelationalCode.liftBody_instantiate line 324
79. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.rename line 341
80. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.base_sorted line 344
81. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.base_mode line 347
82. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.queryBody_family line 349
83. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.goodBody_family line 355
84. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.pair_typed line 360
85. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.rawTop_typed line 372
86. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.point_typed line 376
87. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.bundle_typed line 387
88. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.diamond_formula line 396
89. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.partBody_family line 410
90. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.part_typed line 426
91. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.part_evaluation line 435
92. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.sb_formula line 445
93. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.liftBody_family line 456
94. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.lift_typed line 473
95. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.lift_evaluation line 481
96. theorem OAI.PureTypeSystem.Labelled.DoubleCode.accessBody_rename line 495
97. theorem OAI.PureTypeSystem.Labelled.DoubleCode.accessBody_subst line 501
98. theorem OAI.PureTypeSystem.Labelled.DoubleCode.access_rename line 508
99. theorem OAI.PureTypeSystem.Labelled.DoubleCode.access_subst line 514
100. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerMap_rename line 520
101. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerMap_subst line 525
102. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recoverAccess_rename line 530
103. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recoverAccess_subst line 534
104. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.recoverAccess_formula line 543
105. def OAI.PureTypeSystem.Labelled.RelationalCode.liftEvalBody line 562

     Source documentation

     The genuine logical-element binder in i@lift_m(y).

     def liftEvalBody (L : LogicCode S) (KY KP : QuantifierCode S) (A m i : Expr S) :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierCode, OAI.PureTypeSystem.Labelled.Expr

106. def OAI.PureTypeSystem.Labelled.RelationalCode.predLift line 566
107. def OAI.PureTypeSystem.Labelled.RelationalCode.predLiftMap line 569

     Source documentation

     The data parameter binder, not an assumed semantic universal.

     def predLiftMap (L : LogicCode S) (KY KP : QuantifierCode S) (A i : Expr S) :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierCode, OAI.PureTypeSystem.Labelled.Expr

108. def OAI.PureTypeSystem.Labelled.RelationalCode.recoverLift line 572
109. def OAI.PureTypeSystem.Labelled.RelationalCode.recoverLiftBody line 574
110. def OAI.PureTypeSystem.Labelled.RelationalCode.probeFor line 579

     Source documentation

     The source z_i: the body abstracts z:Z, then w:Single(z↓). No distinguished A or m occurs in this term.

     def probeFor (L : LogicCode S) (KY KP : QuantifierCode S) (i : Expr S) :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierCode, OAI.PureTypeSystem.Labelled.Expr

111. def OAI.PureTypeSystem.Labelled.RelationalCode.le line 582
112. theorem OAI.PureTypeSystem.Labelled.RelationalCode.liftEvalBody_rename line 584
113. theorem OAI.PureTypeSystem.Labelled.RelationalCode.predLift_rename line 589
114. theorem OAI.PureTypeSystem.Labelled.RelationalCode.predLiftMap_rename line 592
115. theorem OAI.PureTypeSystem.Labelled.RelationalCode.recoverLift_rename line 596
116. theorem OAI.PureTypeSystem.Labelled.RelationalCode.recoverLiftBody_rename line 600
117. theorem OAI.PureTypeSystem.Labelled.RelationalCode.liftEvalBody_subst line 604
118. theorem OAI.PureTypeSystem.Labelled.RelationalCode.predLift_subst line 609
119. theorem OAI.PureTypeSystem.Labelled.RelationalCode.predLiftMap_subst line 612
120. theorem OAI.PureTypeSystem.Labelled.RelationalCode.recoverLift_subst line 616
121. theorem OAI.PureTypeSystem.Labelled.RelationalCode.recoverLiftBody_subst line 620
122. theorem OAI.PureTypeSystem.Labelled.RelationalCode.liftEvalBody_instantiate line 624
123. theorem OAI.PureTypeSystem.Labelled.RelationalCode.predLiftMap_instantiate line 629
124. theorem OAI.PureTypeSystem.Labelled.RelationalCode.recoverLiftBody_instantiate line 634
125. theorem OAI.PureTypeSystem.Labelled.ProbeCode.uniform_rename line 643
126. theorem OAI.PureTypeSystem.Labelled.ProbeCode.uniform_subst line 650
127. theorem OAI.PureTypeSystem.Labelled.RelationalCode.probeFor_rename line 660
128. theorem OAI.PureTypeSystem.Labelled.RelationalCode.probeFor_subst line 668
129. theorem OAI.PureTypeSystem.Labelled.RelationalCode.le_rename line 678
130. theorem OAI.PureTypeSystem.Labelled.RelationalCode.le_subst line 682
131. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.liftEvalBody_family line 698
132. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.predLift_typed line 715
133. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.predLiftMap_typed line 724
134. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.recoverLift_formula line 740
135. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.recoverLiftBody_family line 747
136. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.probeFor_typed line 760
137. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.le_formula line 772
138. def OAI.PureTypeSystem.Labelled.RelationalCode.leBody line 783

     Source documentation

     Binder i:P_X for le(i,x).

     def leBody (L : LogicCode S) (KY KP : QuantifierCode S) (x : Expr S) :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierCode, OAI.PureTypeSystem.Labelled.Expr

139. def OAI.PureTypeSystem.Labelled.RelationalCode.xCompareBody line 785
140. def OAI.PureTypeSystem.Labelled.RelationalCode.xCompare line 787
141. theorem OAI.PureTypeSystem.Labelled.RelationalCode.leBody_rename line 790
142. theorem OAI.PureTypeSystem.Labelled.RelationalCode.leBody_subst line 796
143. theorem OAI.PureTypeSystem.Labelled.RelationalCode.leBody_instantiate line 803
144. theorem OAI.PureTypeSystem.Labelled.RelationalCode.xCompareBody_rename line 807
145. theorem OAI.PureTypeSystem.Labelled.RelationalCode.xCompareBody_subst line 812
146. theorem OAI.PureTypeSystem.Labelled.RelationalCode.xCompareBody_instantiate line 817
147. theorem OAI.PureTypeSystem.Labelled.RelationalCode.xCompare_rename line 823
148. theorem OAI.PureTypeSystem.Labelled.RelationalCode.xCompare_subst line 829
149. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.leBody_family line 842
150. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompareBody_family line 854
151. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_formula line 859
152. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_elim line 867
153. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_intro line 879
154. def OAI.PureTypeSystem.Labelled.RelationalCode.extStep line 912
155. def OAI.PureTypeSystem.Labelled.RelationalCode.extAtBody line 915
156. def OAI.PureTypeSystem.Labelled.RelationalCode.extAt line 918
157. def OAI.PureTypeSystem.Labelled.RelationalCode.extBody line 920
158. def OAI.PureTypeSystem.Labelled.RelationalCode.extensional line 923
159. def OAI.PureTypeSystem.Labelled.RelationalCode.validStep line 925
160. def OAI.PureTypeSystem.Labelled.RelationalCode.validAtBody line 928
161. def OAI.PureTypeSystem.Labelled.RelationalCode.validAt line 931
162. def OAI.PureTypeSystem.Labelled.RelationalCode.validBody line 933
163. def OAI.PureTypeSystem.Labelled.RelationalCode.valid line 936
164. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extStep_rename line 939
165. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extStep_subst line 945
166. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extAtBody_rename line 951
167. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extAtBody_subst line 957
168. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extAtBody_instantiate line 963
169. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extAt_rename line 968
170. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extAt_subst line 974
171. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extBody_rename line 980
172. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extBody_subst line 986
173. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extBody_instantiate line 992
174. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extensional_rename line 997
175. theorem OAI.PureTypeSystem.Labelled.RelationalCode.extensional_subst line 1003
176. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validStep_rename line 1009
177. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validStep_subst line 1015
178. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validAtBody_rename line 1021
179. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validAtBody_subst line 1027
180. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validAtBody_instantiate line 1033
181. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validAt_rename line 1038
182. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validAt_subst line 1044
183. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validBody_rename line 1050
184. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validBody_subst line 1056
185. theorem OAI.PureTypeSystem.Labelled.RelationalCode.validBody_instantiate line 1062
186. theorem OAI.PureTypeSystem.Labelled.RelationalCode.valid_rename line 1067
187. theorem OAI.PureTypeSystem.Labelled.RelationalCode.valid_subst line 1073
188. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.x_typed_rename line 1092
189. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_refl line 1098
190. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_symm line 1106
191. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_trans line 1119
192. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.xCompare_round line 1142
193. theorem OAI.PureTypeSystem.Labelled.RelationalCode.x_type_rename line 1158
194. theorem OAI.PureTypeSystem.Labelled.RelationalCode.p_type_rename line 1163
195. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extStep_formula line 1175
196. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.validStep_formula line 1184
197. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extAtBody_family line 1192
198. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extAt_formula line 1206
199. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extBody_family line 1215
200. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extensional_formula line 1226
201. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.validAtBody_family line 1234
202. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.validAt_formula line 1248
203. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.validBody_family line 1257
204. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.valid_formula line 1268
205. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extAt_intro line 1287
206. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extAt_elim_one line 1302
207. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extensional_intro line 1314
208. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extensional_elim_one line 1328
209. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.validAt_intro line 1339
210. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.validAt_elim_one line 1354
211. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.valid_intro line 1366
212. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.valid_elim_one line 1380
213. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extensional_elim line 1391
214. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.valid_elim line 1403
215. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.p_typed_rename line 1425
216. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extStep_respect line 1430
217. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.predComparison_rename line 1450
218. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extAt_respect line 1459
219. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.extensional_respect line 1476

     Source documentation

     Manuscript ExtC: predicate comparison respects the exact Ext formula.

     theorem extensional_respect {i c : Expr S}
         (hi : HasType P Γ i (R.channel.predicateType R.probe.carrier)) (mi : WellModed γ i .data)
         (hc : HasType P Γ c (R.channel.predicateType R.probe.carrier)) (mc : WellModed γ c .data)
         (he : Proves P Γ γ (R.channel.predCompare L.code KY.code R.probe.carrier i c)) :
         Equivalent P Γ γ (R.extensional L.code KY.code KP.code i) (R.extensional L.code KY.code KP.code c) := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Proves, OAI.PureTypeSystem.Labelled.Equivalent

220. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.rename_comp line 1496
221. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.subst_rename line 1498
222. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.rename_subst line 1501
223. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.instantiate_raise line 1504
224. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.firstType_rename line 1506
225. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.firstType_subst line 1509
226. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.middleType_rename line 1512
227. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.middleType_subst line 1515
228. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.carrier_rename line 1518
229. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.carrier_subst line 1521
230. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.bitInner_rename line 1524
231. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.bitInner_subst line 1527
232. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.bitOuter_rename line 1530
233. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.bitOuter_subst line 1533
234. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.observe_rename line 1536
235. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.observe_subst line 1539
236. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.tagged_rename line 1542
237. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.tagged_subst line 1545