Commit dea6eff0 authored by nipkow's avatar nipkow
Browse files

simplified proof

parent 556e4a005c15
......@@ -18,7 +18,7 @@ proof(induction F arbitrary: \<Gamma> \<Delta>)
ultimately show ?case by blast
next
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