Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. R : Alph List Alph List

  3. Fin(Alph)

  4. EquivRel(Alph List;x,y.x R y)

  5. Fin(x,y:(Alph List)//(x R y))

  6. x,y,z:Alph List. x R y (z @ x) R (z @ y)

  7. g : x,y:(Alph List)//(x R y)

  8. Fin(x,y:(Alph List)//(x R y) x,y:(Alph List)//(x R y))

Conclusion:

x,y:x,y:(Alph List)//(x R y). Dec(x Rg y)

Applied Tactic: Assert a:Alph. x:x,y:(Alph List)//(x R y). (a::x) x,y:(Alph List)//(x R y)
Generated subgoals:

1. a:Alph. x:x,y:(Alph List)//(x R y). (a::x) x,y:(Alph List)//(x R y)

2. x,y:x,y:(Alph List)//(x R y). Dec(x Rg y)