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