equal
deleted
inserted
replaced
7 --defined by a combination of induction and coinduction |
7 --defined by a combination of induction and coinduction |
8 *) |
8 *) |
9 |
9 |
10 (*** findRel: basic laws ****) |
10 (*** findRel: basic laws ****) |
11 |
11 |
12 val findRel_LConsE = |
12 val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p"; |
13 findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p"; |
|
14 |
13 |
15 AddSEs [findRel_LConsE]; |
14 AddSEs [findRel_LConsE]; |
16 |
15 |
17 |
16 |
18 Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"; |
17 Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"; |