equal
deleted
inserted
replaced
394 using fcb1 fresh perm1 perm2 |
394 using fcb1 fresh perm1 perm2 |
395 apply(simp_all add: fresh_star_def) |
395 apply(simp_all add: fresh_star_def) |
396 done |
396 done |
397 |
397 |
398 lemma Abs_lst1_fcb2': |
398 lemma Abs_lst1_fcb2': |
399 fixes a b :: "'a::at" |
399 fixes a b :: "'a::at_base" |
400 and x y :: "'b :: fs" |
400 and x y :: "'b :: fs" |
401 and c::"'c :: fs" |
401 and c::"'c :: fs" |
402 assumes e: "[[atom a]]lst. x = [[atom b]]lst. y" |
402 assumes e: "[[atom a]]lst. x = [[atom b]]lst. y" |
403 and fcb1: "atom a \<sharp> f a x c" |
403 and fcb1: "atom a \<sharp> f a x c" |
404 and fresh: "{atom a, atom b} \<sharp>* c" |
404 and fresh: "{atom a, atom b} \<sharp>* c" |