equal
deleted
inserted
replaced
132 apply (rules intro: NF.Abs) |
132 apply (rules intro: NF.Abs) |
133 done |
133 done |
134 |
134 |
135 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" |
135 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" |
136 apply (induct set: NF) |
136 apply (induct set: NF) |
137 apply (subst app_last) |
137 apply (simplesubst app_last) --{*Using @{text subst} makes extraction fail*} |
138 apply (rule exI) |
138 apply (rule exI) |
139 apply (rule conjI) |
139 apply (rule conjI) |
140 apply (rule rtrancl_refl) |
140 apply (rule rtrancl_refl) |
141 apply (rule NF.App) |
141 apply (rule NF.App) |
142 apply (drule listall_conj1) |
142 apply (drule listall_conj1) |