src/FOL/IFOL.thy

   \<open>P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R\<close>
   \<open>(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P\<close>
   \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close>
   by iprover+
 
+lemma subst_all:
+  \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
+proof (rule equal_intr_rule)
+  assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close>
+  show \<open>PROP P(a)\<close>
+    by (rule *) (rule refl)
+next
+  fix x
+  assume \<open>PROP P(a)\<close> and \<open>x = a\<close>
+  from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
+    by (rule eq_reflection)
+  with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
+    by simp
+qed
+
+lemma subst_all':
+  \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
+proof (rule equal_intr_rule)
+  assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close>
+  show \<open>PROP P(a)\<close>
+    by (rule *) (rule refl)
+next
+  fix x
+  assume \<open>PROP P(a)\<close> and \<open>a = x\<close>
+  from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
+    by (rule eq_reflection)
+  with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
+    by simp
+qed
+
 
 subsubsection \<open>Conversion into rewrite rules\<close>
 
 lemma P_iff_F: \<open>\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)\<close>
   by iprover