equal
deleted
inserted
replaced
82 apply clarify |
82 apply clarify |
83 apply (drule bspec, assumption) |
83 apply (drule bspec, assumption) |
84 apply (erule mp) |
84 apply (erule mp) |
85 apply clarify |
85 apply clarify |
86 apply (drule_tac r=beta in conversepI) |
86 apply (drule_tac r=beta in conversepI) |
87 apply (drule_tac r="beta^--1" in ex_step1I, assumption) |
87 apply (drule_tac r="beta\<inverse>\<inverse>" in ex_step1I, assumption) |
88 apply clarify |
88 apply clarify |
89 apply (rename_tac us) |
89 apply (rename_tac us) |
90 apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
90 apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
91 apply force |
91 apply force |
92 apply (rename_tac u ts) |
92 apply (rename_tac u ts) |