Dominik
Dietrich
Home
Publications
Teaching
News
CIAO 2009 Workshop
Please enter the proof script below
theory pi3 conjecture stepcase "(cat(cons(X,L),empty) = cons(X,L))" proof "cat(cons(x,l),empty) = cons(x,cat(l,empty))" by cat2 .="cons(x,cat(empty,l))" by inducthyp .="cons(x,l)" by cat2 qed