Inference at * 1 0 4 2 1 2 1 1 
Iof proof for Lemma eq int cases test:



1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. bb : 
8. (i = j) = bb
9. P(if (i = j) then x else y fi )
10.   Type
11. (i = j)  
12. bb:. ((i = j) = bb)  Type
13. z : 
14. (i = j) = z
  P(if z then x else y fi )   

latex

 by (\p.let i = get_int_arg `i` p in 
((OnHyps [i+1;i;-3;-3;-3] Thin) 
CollapseTHEN (
CAddHiddenLabel `functionality`)) p) 

latex

C1: .....functionality..... NILNIL

C1: 7. P(if (i = j) then x else y fi )
C1: 8. z : 
C1: 9. (i = j) = z
C1:   P(if z then x else y fi )  
C.

Definitions

x:A. B(x), t  T, if b then t else f fi , f(a), (i = j), s = t, , , , x:AB(x), Type