x.b(x))(a)
A,B:Type, a:A, b:(A
B). let x = a in b(x) 
B| No mentions to report in SUPPORTjlc | |
| let | Def let x = a in b(x) == (x.b(x))(a) |
| Thm* A,B:Type, a:A, b:(AB). let x = a in b(x) B |
| Syntax: | let x = a in b(x) | has structure: | let(a; x.b(x)) |
About:
 |  |  |  |  |  |  |