[STATEMENT]
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qfree p; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
imp ?p ?q \<equiv> if ?p = F \<or> ?q = T \<or> ?p = ?q then T else if ?p = T then ?q else if ?q = F then MIR.not ?p else Imp ?p ?q

goal (1 subgoal):
 1. \<lbrakk>qfree p; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)
[PROOF STEP]
by (cases "p=F \<or> q=T",simp_all add: imp_def)