equal
deleted
inserted
replaced
413 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
413 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
414 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
414 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
415 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
415 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
416 apply(blast) |
416 apply(blast) |
417 apply(blast) |
417 apply(blast) |
418 oops |
418 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
419 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
|
420 apply(erule conjE)+ |
|
421 apply(erule Abs_lst_fcb2) |
|
422 apply(simp add: Abs_fresh_star) |
|
423 apply(simp add: Abs_fresh_star) |
|
424 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
425 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
426 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
427 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
428 apply(blast) |
|
429 apply(blast) |
|
430 done |
419 |
431 |
420 end |
432 end |
421 |
433 |
422 |
434 |
423 |
435 |