A,A':Type.
strong-subtype(A;A')
(B:(A
Type), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'),
(f,g:a:A fp-> B(a). (a:A. B(a) 
r C(a)) f g f g) A,A':Type.
strong-subtype(A;A')
(B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'),
(f,g:a:A fp-> B(a). (a:A. B(a) r C(a)) f g f g)| By: |
|
None
About:
 |  |  |  |  |