130def parameterIdentityEqual =
131 (lambda unrestricted left : (family ParameterIdentity) .
132 (lambda unrestricted right : (family ParameterIdentity) .
133 (eliminate
134 ParameterIdentity
135 (lambda unrestricted current : (family ParameterIdentity) . (family StdBool))
136 left
137 (branch
138 ParameterIdentityOf
139 leftComponents
140 .
141 (eliminate
142 ParameterIdentity
143 (lambda unrestricted current : (family ParameterIdentity) . (family StdBool))
144 right
145 (branch
146 ParameterIdentityOf
147 rightComponents
148 .
149 (app
150 (eliminate
151 StdList
152 (lambda unrestricted current : (family StdList Bytes) .
153 (pi unrestricted other : (family StdList Bytes) . (family StdBool)))
154 leftComponents
155 (branch
156 StdListEmpty
157 .
158 (lambda unrestricted other : (family StdList Bytes) .
159 (stdListIsEmpty Bytes other)))
160 (branch
161 StdListCons
162 head
163 tail
164 induction
165 .
166 (lambda unrestricted other : (family StdList Bytes) .
167 (eliminate
168 StdList
169 (lambda unrestricted current : (family StdList Bytes) . (family StdBool))
170 other
171 (branch StdListEmpty . (constructor StdBool StdFalse))
172 (branch
173 StdListCons
174 otherHead
175 otherTail
176 otherInduction
177 .
178 (stdBoolAnd
179 (stdBoolFromNatural (bytes-equal head otherHead))
180 (induction otherTail)))))))
181 rightComponents)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.