E:(T
T
). (x,y:T. E(x,y) 
x = y) 
(i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) 
s) 
(inr(i) s))
xs.InjCase(x; a. E(a;i), E(a;i)))
is mentioned by
| Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s)) | [assert-member-paren] |
Try larger context:
Graphs