136   "Quot_True x \<equiv> True"

   136   "Quot_True x \<equiv> True"

   137 

   137 

   138 lemma 

   138 lemma 

   139   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"

   139   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"

   140   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"

   140   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"

   141   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True  (P x))"

   142   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True  (P x))"

   142   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"

   143   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"

   143 by (simp_all add: Quot_True_def ext)

   144 by (simp_all add: Quot_True_def ext)

   144 

   145 

   145 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"

   146 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"