equal
deleted
inserted
replaced
157 apply (rule impI [THEN allI [THEN allI]]) |
157 apply (rule impI [THEN allI [THEN allI]]) |
158 apply (erule beta.induct) |
158 apply (erule beta.induct) |
159 apply (slowsimp intro: rtrancl_eta_subst eta_subst) |
159 apply (slowsimp intro: rtrancl_eta_subst eta_subst) |
160 apply (blast intro: rtrancl_eta_AppL) |
160 apply (blast intro: rtrancl_eta_AppL) |
161 apply (blast intro: rtrancl_eta_AppR) |
161 apply (blast intro: rtrancl_eta_AppR) |
162 apply simp; |
162 apply simp |
163 apply (slowsimp intro: rtrancl_eta_Abs free_beta |
163 apply (slowsimp intro: rtrancl_eta_Abs free_beta |
164 iff del: dB.distinct simp: dB.distinct) (*23 seconds?*) |
164 iff del: dB.distinct simp: dB.distinct) (*23 seconds?*) |
165 done |
165 done |
166 |
166 |
167 lemma confluent_beta_eta: "confluent (sup beta eta)" |
167 lemma confluent_beta_eta: "confluent (sup beta eta)" |