Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. E:T 
T 
. (x,y:T. Dec(E[x;y])) 
(
f:T T 
. x,y:T. 
(x f y) E[x;y])
Applied Tactic: (Unfolds ``infix_ap so_apply`` 0
THENM GenRepD ...a)
Generated subgoals:1. f:T T . x,y:T. (f x y) E x y2. Dec(E x y)