Refl(A*;x,y.x L-induced Equiv y) Sym x,y:A*. x L-induced Equiv y Trans x,y:A*. x L-induced Equiv y Refl(A*;x,y.x L-induced Equiv y)
& Sym x,y:A*. x L-induced Equiv y
& Trans x,y:A*. x L-induced Equiv y| 1 | Refl(A*;x,y.x L-induced Equiv y) |
| 2 | Sym x,y:A*. x L-induced Equiv y |
| 3 | Trans x,y:A*. x L-induced Equiv y |
About:
 |  |  |