| changeset 796 | 64f9c76f70c7 |
| parent 794 | f0a78fda343f |
| child 797 | 35436401f00d |
| 795:a28f805df355 | 796:64f9c76f70c7 |
|---|---|
598 |
598 |
599 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa" |
599 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa" |
600 apply (lifting list.cases(2)) |
600 apply (lifting list.cases(2)) |
601 done |
601 done |
602 |
602 |
603 thm quot_respect |
|
604 |
|
603 |
605 |
604 end |
606 end |