Commit 3965bae4 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files


......@@ -18,7 +18,7 @@ proof(induction F arbitrary: \<Gamma> \<Delta>)
ultimately show ?case by blast
case Bot
have "\<bottom>, \<bottom>, \<Gamma> \<Rightarrow> \<Delta> \<Longrightarrow> \<bottom>, \<Gamma> \<Rightarrow> \<Delta>" by(induction "\<bottom>, \<bottom>, \<Gamma>" \<Delta> rule: SCp.induct; blast)
have "\<bottom>, \<bottom>, \<Gamma> \<Rightarrow> \<Delta> \<Longrightarrow> \<bottom>, \<Gamma> \<Rightarrow> \<Delta>" by(blast)
moreover have "(\<Gamma> \<Rightarrow> \<bottom>, \<bottom>, \<Delta> \<Longrightarrow> \<Gamma> \<Rightarrow> \<bottom>, \<Delta>)"
using Bot_delR by fastforce
ultimately show ?case by blast
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment