Inference at * 2 1 
Iof proof for Lemma subtype rel dep product iff:

.....unproved Inclusion subgoal..... NILNIL

1. A : Type
2. B : AType
3. C : Type
4. D : CType
5. A r C
6. (a:A  B(a)) r (c:C  D(c))
7. a : A
8. x : B(a)
  x  D(a) 

latex

 by Assert <a, x>  (c:C  D(c)) 

latex

 1: .....assertion..... NILNIL

 1:   <a, x>  (c:C  D(c))
 2: 

 2: 9. <a, x>  (c:C  D(c))
 2:   x  D(a)
 .

Definitions

t  T, x:A  B(x), x(s), <a, b>