Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. R:Alph List 
Alph List 
. n:
. L:Alph List 
. m:.
(x:Alph List. R x x)
(x,y:Alph List. R x y 
R y x)
(x,y,z:Alph List. R x y R y z R x z)
(x,y,z:Alph List. R x y R (z @ x) (z @ y))
(
w:n Alph List. l:Alph List. i:n. R l (w i))
(v:m Alph List. l:Alph List. 
(L l) 
(i:m. R l (v i)))
Fin(Alph)
(x,y:Alph List. Dec(l:Alph List. L (l @ x) = L (l @ y)))
Applied Tactic: UnivCD THENW Auto
Generated subgoals:1. Dec(l:Alph List. L (l @ x) = L (l @ y))