equal
deleted
inserted
replaced
144 apply (iprover intro: NF.Abs) |
144 apply (iprover intro: NF.Abs) |
145 done |
145 done |
146 |
146 |
147 lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
147 lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
148 apply (induct set: NF) |
148 apply (induct set: NF) |
149 apply (simplesubst app_last) \<comment>\<open>Using \<open>subst\<close> makes extraction fail\<close> |
149 apply (simplesubst app_last) \<comment> \<open>Using \<open>subst\<close> makes extraction fail\<close> |
150 apply (rule exI) |
150 apply (rule exI) |
151 apply (rule conjI) |
151 apply (rule conjI) |
152 apply (rule rtranclp.rtrancl_refl) |
152 apply (rule rtranclp.rtrancl_refl) |
153 apply (rule NF.App) |
153 apply (rule NF.App) |
154 apply (drule listall_conj1) |
154 apply (drule listall_conj1) |