---

Step * of Lemma strong_subtype_decidable_eq

A,B:Type.  (strong-subtype(A;B)  dec_eq_type(B)  dec_eq_type(A))
BY
{ (RepUR ``dec_eq_type strong-subtype decidable`` 0 THEN Auto) }

1
1. A : Type@i'
2. B : Type@i'
3. (A r B) c ({b:B| a:A. (b = a)}  r A)@i
4. x,y:B.  ((x = y)  ((x = y)))@i
5. x : A@i
6. y : A@i
 (x = y)  ((x = y))


\mforall{}A,B:Type.    (strong-subtype(A;B)  {}\mRightarrow{}  dec\_eq\_type(B)  {}\mRightarrow{}  dec\_eq\_type(A))


By

(RepUR  ``dec\_eq\_type  strong-subtype  decidable``  0  THEN  Auto)



Home Index