more symbols;
authorwenzelm
Mon Nov 27 10:36:43 2017 +0100 (19 months ago)
changeset 670944a2563645635
parent 67093 835a2ab92c3d
child 67095 91ffe1f8bf5c
more symbols;
src/HOL/Tools/rewrite_hol_proof.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 27 10:21:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 27 10:36:43 2017 +0100
     1.3 @@ -19,288 +19,288 @@
     1.4  
     1.5    (** eliminate meta-equality rules **)
     1.6  
     1.7 -  [\<open>(equal_elim % x1 % x2 %%
     1.8 -      (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%
     1.9 -        (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==
    1.10 -    (iffD1 % A % B %%
    1.11 -      (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))\<close>,
    1.12 +  [\<open>(equal_elim \<cdot> x1 \<cdot> x2 \<bullet>
    1.13 +      (combination \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Trueprop \<cdot> x3 \<cdot> A \<cdot> B \<bullet>
    1.14 +        (axm.reflexive \<cdot> TYPE('T3) \<cdot> x4) \<bullet> prf1)) \<equiv>
    1.15 +    (iffD1 \<cdot> A \<cdot> B \<bullet>
    1.16 +      (meta_eq_to_obj_eq \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<bullet> arity_type_bool \<bullet> prf1))\<close>,
    1.17  
    1.18 -   \<open>(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%
    1.19 -      (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%
    1.20 -        (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==
    1.21 -    (iffD2 % A % B %%
    1.22 -      (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))\<close>,
    1.23 +   \<open>(equal_elim \<cdot> x1 \<cdot> x2 \<bullet> (axm.symmetric \<cdot> TYPE('T1) \<cdot> x3 \<cdot> x4 \<bullet>
    1.24 +      (combination \<cdot> TYPE('T2) \<cdot> TYPE('T3) \<cdot> Trueprop \<cdot> x5 \<cdot> A \<cdot> B \<bullet>
    1.25 +        (axm.reflexive \<cdot> TYPE('T4) \<cdot> x6) \<bullet> prf1))) \<equiv>
    1.26 +    (iffD2 \<cdot> A \<cdot> B \<bullet>
    1.27 +      (meta_eq_to_obj_eq \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<bullet> arity_type_bool \<bullet> prf1))\<close>,
    1.28  
    1.29 -   \<open>(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %%
    1.30 -      (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==
    1.31 -    (cong % TYPE('T) % TYPE('U) % f % g % x % y %%
    1.32 -      (OfClass type_class % TYPE('T)) %% prfU %%
    1.33 -      (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %%
    1.34 -      (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))\<close>,
    1.35 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> x1 \<cdot> x2 \<bullet> prfU \<bullet>
    1.36 +      (combination \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet> prf1 \<bullet> prf2)) \<equiv>
    1.37 +    (cong \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet>
    1.38 +      (OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
    1.39 +      (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
    1.40 +      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
    1.41  
    1.42 -   \<open>(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %%
    1.43 -      (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==
    1.44 -    (HOL.trans % TYPE('T) % x % y % z %% prfT %%
    1.45 -      (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %%
    1.46 -      (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))\<close>,
    1.47 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet>
    1.48 +      (axm.transitive \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prf1 \<bullet> prf2)) \<equiv>
    1.49 +    (HOL.trans \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prfT \<bullet>
    1.50 +      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf1) \<bullet>
    1.51 +      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> y \<cdot> z \<bullet> prfT \<bullet> prf2))\<close>,
    1.52  
    1.53 -   \<open>(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) ==
    1.54 -    (HOL.refl % TYPE('T) % x %% prfT)\<close>,
    1.55 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> x \<bullet> prfT \<bullet> (axm.reflexive \<cdot> TYPE('T) \<cdot> x)) \<equiv>
    1.56 +    (HOL.refl \<cdot> TYPE('T) \<cdot> x \<bullet> prfT)\<close>,
    1.57  
    1.58 -   \<open>(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%
    1.59 -      (axm.symmetric % TYPE('T) % x % y %% prf)) ==
    1.60 -    (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))\<close>,
    1.61 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
    1.62 +      (axm.symmetric \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prf)) \<equiv>
    1.63 +    (sym \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf))\<close>,
    1.64  
    1.65 -   \<open>(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %%
    1.66 -      (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==
    1.67 -    (ext % TYPE('T) % TYPE('U) % f % g %%
    1.68 -      (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %%
    1.69 -      (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %%
    1.70 -         (OfClass type_class % TYPE('U)) %% (prf % x)))\<close>,
    1.71 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> x1 \<cdot> x2 \<bullet> prfTU \<bullet>
    1.72 +      (abstract_rule \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet> prf)) \<equiv>
    1.73 +    (ext \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet>
    1.74 +      (OfClass type_class \<cdot> TYPE('T)) \<bullet> (OfClass type_class \<cdot> TYPE('U)) \<bullet>
    1.75 +      (\<^bold>\<lambda>(x::'T). meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> f x \<cdot> g x \<bullet>
    1.76 +         (OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
    1.77  
    1.78 -   \<open>(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%
    1.79 -      (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf\<close>,
    1.80 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
    1.81 +      (eq_reflection \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf)) \<equiv> prf\<close>,
    1.82  
    1.83 -   \<open>(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%
    1.84 -      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%
    1.85 -        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%
    1.86 -          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==
    1.87 -    (iffD1 % A = C % B = D %%
    1.88 -      (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%
    1.89 -        prfT %% arity_type_bool %%
    1.90 -        (cong % TYPE('T) % TYPE('T=>bool) %
    1.91 -          (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%
    1.92 -          prfT %% (OfClass type_class % TYPE('T=>bool)) %%
    1.93 -          (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%
    1.94 -             (OfClass type_class % TYPE('T=>'T=>bool))) %%
    1.95 -          (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%
    1.96 -        (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%
    1.97 -      (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))\<close>,
    1.98 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet> (equal_elim \<cdot> x3 \<cdot> x4 \<bullet>
    1.99 +      (combination \<cdot> TYPE('T) \<cdot> TYPE(prop) \<cdot> x7 \<cdot> x8 \<cdot> C \<cdot> D \<bullet>
   1.100 +        (combination \<cdot> TYPE('T) \<cdot> TYPE('T3) \<cdot> op \<equiv> \<cdot> op \<equiv> \<cdot> A \<cdot> B \<bullet>
   1.101 +          (axm.reflexive \<cdot> TYPE('T4) \<cdot> op \<equiv>) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3)) \<equiv>
   1.102 +    (iffD1 \<cdot> A = C \<cdot> B = D \<bullet>
   1.103 +      (cong \<cdot> TYPE('T) \<cdot> TYPE(bool) \<cdot> op = A \<cdot> op = B \<cdot> C \<cdot> D \<bullet>
   1.104 +        prfT \<bullet> arity_type_bool \<bullet>
   1.105 +        (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
   1.106 +          (op = :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> (op = :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
   1.107 +          prfT \<bullet> (OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
   1.108 +          (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> (op = :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
   1.109 +             (OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
   1.110 +          (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
   1.111 +        (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
   1.112 +      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> C \<bullet> prfT \<bullet> prf3))\<close>,
   1.113  
   1.114 -   \<open>(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%
   1.115 -      (axm.symmetric % TYPE('T2) % x5 % x6 %%
   1.116 -        (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%
   1.117 -          (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%
   1.118 -            (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==
   1.119 -    (iffD2 % A = C % B = D %%
   1.120 -      (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%
   1.121 -        prfT %% arity_type_bool %%
   1.122 -        (cong % TYPE('T) % TYPE('T=>bool) %
   1.123 -          (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%
   1.124 -          prfT %% (OfClass type_class % TYPE('T=>bool)) %%
   1.125 -          (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%
   1.126 -             (OfClass type_class % TYPE('T=>'T=>bool))) %%
   1.127 -          (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%
   1.128 -        (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%
   1.129 -      (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))\<close>,
   1.130 +   \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet> (equal_elim \<cdot> x3 \<cdot> x4 \<bullet>
   1.131 +      (axm.symmetric \<cdot> TYPE('T2) \<cdot> x5 \<cdot> x6 \<bullet>
   1.132 +        (combination \<cdot> TYPE('T) \<cdot> TYPE(prop) \<cdot> x7 \<cdot> x8 \<cdot> C \<cdot> D \<bullet>
   1.133 +          (combination \<cdot> TYPE('T) \<cdot> TYPE('T3) \<cdot> op \<equiv> \<cdot> op \<equiv> \<cdot> A \<cdot> B \<bullet>
   1.134 +            (axm.reflexive \<cdot> TYPE('T4) \<cdot> op \<equiv>) \<bullet> prf1) \<bullet> prf2)) \<bullet> prf3)) \<equiv>
   1.135 +    (iffD2 \<cdot> A = C \<cdot> B = D \<bullet>
   1.136 +      (cong \<cdot> TYPE('T) \<cdot> TYPE(bool) \<cdot> op = A \<cdot> op = B \<cdot> C \<cdot> D \<bullet>
   1.137 +        prfT \<bullet> arity_type_bool \<bullet>
   1.138 +        (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
   1.139 +          (op = :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> (op = :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
   1.140 +          prfT \<bullet> (OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
   1.141 +          (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> (op = :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
   1.142 +             (OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
   1.143 +          (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
   1.144 +        (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
   1.145 +      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> B \<cdot> D \<bullet> prfT \<bullet> prf3))\<close>,
   1.146  
   1.147     (** rewriting on bool: insert proper congruence rules for logical connectives **)
   1.148  
   1.149     (* All *)
   1.150  
   1.151 -   \<open>(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%
   1.152 -      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.153 -      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.154 -    (allI % TYPE('a) % Q %% prfa %%
   1.155 -      (Lam x.
   1.156 -          iffD1 % P x % Q x %% (prf % x) %%
   1.157 -           (spec % TYPE('a) % P % x %% prfa %% prf')))\<close>,
   1.158 +   \<open>(iffD1 \<cdot> All P \<cdot> All Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> All \<cdot> All \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.159 +      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
   1.160 +      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
   1.161 +    (allI \<cdot> TYPE('a) \<cdot> Q \<bullet> prfa \<bullet>
   1.162 +      (\<^bold>\<lambda>x.
   1.163 +          iffD1 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet>
   1.164 +           (spec \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> prf')))\<close>,
   1.165  
   1.166 -   \<open>(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%
   1.167 -      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.168 -      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.169 -    (allI % TYPE('a) % P %% prfa %%
   1.170 -      (Lam x.
   1.171 -          iffD2 % P x % Q x %% (prf % x) %%
   1.172 -           (spec % TYPE('a) % Q % x %% prfa %% prf')))\<close>,
   1.173 +   \<open>(iffD2 \<cdot> All P \<cdot> All Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> All \<cdot> All \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.174 +      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
   1.175 +      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
   1.176 +    (allI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa \<bullet>
   1.177 +      (\<^bold>\<lambda>x.
   1.178 +          iffD2 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet>
   1.179 +           (spec \<cdot> TYPE('a) \<cdot> Q \<cdot> x \<bullet> prfa \<bullet> prf')))\<close>,
   1.180  
   1.181     (* Ex *)
   1.182  
   1.183 -   \<open>(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%
   1.184 -      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.185 -      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.186 -    (exE % TYPE('a) % P % \<exists>x. Q x %% prfa %% prf' %%
   1.187 -      (Lam x H : P x.
   1.188 -          exI % TYPE('a) % Q % x %% prfa %%
   1.189 -           (iffD1 % P x % Q x %% (prf % x) %% H)))\<close>,
   1.190 +   \<open>(iffD1 \<cdot> Ex P \<cdot> Ex Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Ex \<cdot> Ex \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.191 +      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
   1.192 +      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
   1.193 +    (exE \<cdot> TYPE('a) \<cdot> P \<cdot> \<exists>x. Q x \<bullet> prfa \<bullet> prf' \<bullet>
   1.194 +      (\<^bold>\<lambda>x H : P x.
   1.195 +          exI \<cdot> TYPE('a) \<cdot> Q \<cdot> x \<bullet> prfa \<bullet>
   1.196 +           (iffD1 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet> H)))\<close>,
   1.197  
   1.198 -   \<open>(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%
   1.199 -      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.200 -      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.201 -    (exE % TYPE('a) % Q % \<exists>x. P x %% prfa %% prf' %%
   1.202 -      (Lam x H : Q x.
   1.203 -          exI % TYPE('a) % P % x %% prfa %%
   1.204 -           (iffD2 % P x % Q x %% (prf % x) %% H)))\<close>,
   1.205 +   \<open>(iffD2 \<cdot> Ex P \<cdot> Ex Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Ex \<cdot> Ex \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.206 +      (HOL.refl \<cdot> TYPE('T3) \<cdot> x1 \<bullet> prfT3) \<bullet>
   1.207 +      (ext \<cdot> TYPE('a) \<cdot> TYPE(bool) \<cdot> x2 \<cdot> x3 \<bullet> prfa \<bullet> prfb \<bullet> prf)) \<bullet> prf') \<equiv>
   1.208 +    (exE \<cdot> TYPE('a) \<cdot> Q \<cdot> \<exists>x. P x \<bullet> prfa \<bullet> prf' \<bullet>
   1.209 +      (\<^bold>\<lambda>x H : Q x.
   1.210 +          exI \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet>
   1.211 +           (iffD2 \<cdot> P x \<cdot> Q x \<bullet> (prf \<cdot> x) \<bullet> H)))\<close>,
   1.212  
   1.213     (* \<and> *)
   1.214  
   1.215 -   \<open>(iffD1 % A \<and> C % B \<and> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.216 -      (cong % TYPE('T3) % TYPE('T4) % op \<and> % op \<and> % A % B %% prfT3 %% prfT4 %%
   1.217 -        (HOL.refl % TYPE('T5) % op \<and> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.218 -    (conjI % B % D %%
   1.219 -      (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%
   1.220 -      (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))\<close>,
   1.221 +   \<open>(iffD1 \<cdot> A \<and> C \<cdot> B \<and> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.222 +      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> op \<and> \<cdot> op \<and> \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
   1.223 +        (HOL.refl \<cdot> TYPE('T5) \<cdot> op \<and> \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.224 +    (conjI \<cdot> B \<cdot> D \<bullet>
   1.225 +      (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> (conjunct1 \<cdot> A \<cdot> C \<bullet> prf3)) \<bullet>
   1.226 +      (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> (conjunct2 \<cdot> A \<cdot> C \<bullet> prf3)))\<close>,
   1.227  
   1.228 -   \<open>(iffD2 % A \<and> C % B \<and> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.229 -      (cong % TYPE('T3) % TYPE('T4) % op \<and> % op \<and> % A % B %% prfT3 %% prfT4 %%
   1.230 -        (HOL.refl % TYPE('T5) % op \<and> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.231 -    (conjI % A % C %%
   1.232 -      (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%
   1.233 -      (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))\<close>,
   1.234 +   \<open>(iffD2 \<cdot> A \<and> C \<cdot> B \<and> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.235 +      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> op \<and> \<cdot> op \<and> \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
   1.236 +        (HOL.refl \<cdot> TYPE('T5) \<cdot> op \<and> \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.237 +    (conjI \<cdot> A \<cdot> C \<bullet>
   1.238 +      (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> (conjunct1 \<cdot> B \<cdot> D \<bullet> prf3)) \<bullet>
   1.239 +      (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> (conjunct2 \<cdot> B \<cdot> D \<bullet> prf3)))\<close>,
   1.240  
   1.241 -   \<open>(cong % TYPE(bool) % TYPE(bool) % op \<and> A % op \<and> A % B % C %% prfb %% prfb %%
   1.242 -      (HOL.refl % TYPE(bool=>bool) % op \<and> A %% prfbb)) ==
   1.243 -    (cong % TYPE(bool) % TYPE(bool) % op \<and> A % op \<and> A % B % C %% prfb %% prfb %%
   1.244 -      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.245 -        (op \<and> :: bool=>bool=>bool) % (op \<and> :: bool=>bool=>bool) % A % A %%
   1.246 -          prfb %% prfbb %%
   1.247 -          (HOL.refl % TYPE(bool=>bool=>bool) % (op \<and> :: bool=>bool=>bool) %%
   1.248 -             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.249 -          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.250 +   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op \<and> A \<cdot> op \<and> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.251 +      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> op \<and> A \<bullet> prfbb)) \<equiv>
   1.252 +    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op \<and> A \<cdot> op \<and> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.253 +      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
   1.254 +        (op \<and> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op \<and> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
   1.255 +          prfb \<bullet> prfbb \<bullet>
   1.256 +          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op \<and> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
   1.257 +             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
   1.258 +          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
   1.259  
   1.260     (* \<or> *)
   1.261  
   1.262 -   \<open>(iffD1 % A \<or> C % B \<or> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.263 -      (cong % TYPE('T3) % TYPE('T4) % op \<or> % op \<or> % A % B %% prfT3 %% prfT4 %%
   1.264 -        (HOL.refl % TYPE('T5) % op \<or> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.265 -    (disjE % A % C % B \<or> D %% prf3 %%
   1.266 -      (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%
   1.267 -      (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))\<close>,
   1.268 +   \<open>(iffD1 \<cdot> A \<or> C \<cdot> B \<or> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.269 +      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> op \<or> \<cdot> op \<or> \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
   1.270 +        (HOL.refl \<cdot> TYPE('T5) \<cdot> op \<or> \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.271 +    (disjE \<cdot> A \<cdot> C \<cdot> B \<or> D \<bullet> prf3 \<bullet>
   1.272 +      (\<^bold>\<lambda>H : A. disjI1 \<cdot> B \<cdot> D \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H)) \<bullet>
   1.273 +      (\<^bold>\<lambda>H : C. disjI2 \<cdot> D \<cdot> B \<bullet> (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> H)))\<close>,
   1.274  
   1.275 -   \<open>(iffD2 % A \<or> C % B \<or> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.276 -      (cong % TYPE('T3) % TYPE('T4) % op \<or> % op \<or> % A % B %% prfT3 %% prfT4 %%
   1.277 -        (HOL.refl % TYPE('T5) % op \<or> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.278 -    (disjE % B % D % A \<or> C %% prf3 %%
   1.279 -      (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%
   1.280 -      (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))\<close>,
   1.281 +   \<open>(iffD2 \<cdot> A \<or> C \<cdot> B \<or> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.282 +      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> op \<or> \<cdot> op \<or> \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
   1.283 +        (HOL.refl \<cdot> TYPE('T5) \<cdot> op \<or> \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.284 +    (disjE \<cdot> B \<cdot> D \<cdot> A \<or> C \<bullet> prf3 \<bullet>
   1.285 +      (\<^bold>\<lambda>H : B. disjI1 \<cdot> A \<cdot> C \<bullet> (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H)) \<bullet>
   1.286 +      (\<^bold>\<lambda>H : D. disjI2 \<cdot> C \<cdot> A \<bullet> (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> H)))\<close>,
   1.287  
   1.288 -   \<open>(cong % TYPE(bool) % TYPE(bool) % op \<or> A % op \<or> A % B % C %% prfb %% prfb %%
   1.289 -      (HOL.refl % TYPE(bool=>bool) % op \<or> A %% prfbb)) ==
   1.290 -    (cong % TYPE(bool) % TYPE(bool) % op \<or> A % op \<or> A % B % C %% prfb %% prfb %%
   1.291 -      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.292 -        (op \<or> :: bool=>bool=>bool) % (op \<or> :: bool=>bool=>bool) % A % A %%
   1.293 -          prfb %% prfbb %%
   1.294 -          (HOL.refl % TYPE(bool=>bool=>bool) % (op \<or> :: bool=>bool=>bool) %%
   1.295 -             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.296 -          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.297 +   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op \<or> A \<cdot> op \<or> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.298 +      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> op \<or> A \<bullet> prfbb)) \<equiv>
   1.299 +    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op \<or> A \<cdot> op \<or> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.300 +      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
   1.301 +        (op \<or> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op \<or> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
   1.302 +          prfb \<bullet> prfbb \<bullet>
   1.303 +          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op \<or> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
   1.304 +             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
   1.305 +          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
   1.306  
   1.307     (* \<longrightarrow> *)
   1.308  
   1.309 -   \<open>(iffD1 % A \<longrightarrow> C % B \<longrightarrow> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.310 -      (cong % TYPE('T3) % TYPE('T4) % op \<longrightarrow> % op \<longrightarrow> % A % B %% prfT3 %% prfT4 %%
   1.311 -        (HOL.refl % TYPE('T5) % op \<longrightarrow> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.312 -    (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%
   1.313 -      (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))\<close>,
   1.314 +   \<open>(iffD1 \<cdot> A \<longrightarrow> C \<cdot> B \<longrightarrow> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.315 +      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> op \<longrightarrow> \<cdot> op \<longrightarrow> \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
   1.316 +        (HOL.refl \<cdot> TYPE('T5) \<cdot> op \<longrightarrow> \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.317 +    (impI \<cdot> B \<cdot> D \<bullet> (\<^bold>\<lambda>H: B. iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
   1.318 +      (mp \<cdot> A \<cdot> C \<bullet> prf3 \<bullet> (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H))))\<close>,
   1.319  
   1.320 -   \<open>(iffD2 % A \<longrightarrow> C % B \<longrightarrow> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.321 -      (cong % TYPE('T3) % TYPE('T4) % op \<longrightarrow> % op \<longrightarrow> % A % B %% prfT3 %% prfT4 %%
   1.322 -        (HOL.refl % TYPE('T5) % op \<longrightarrow> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.323 -    (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%
   1.324 -      (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))\<close>,
   1.325 +   \<open>(iffD2 \<cdot> A \<longrightarrow> C \<cdot> B \<longrightarrow> D \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.326 +      (cong \<cdot> TYPE('T3) \<cdot> TYPE('T4) \<cdot> op \<longrightarrow> \<cdot> op \<longrightarrow> \<cdot> A \<cdot> B \<bullet> prfT3 \<bullet> prfT4 \<bullet>
   1.327 +        (HOL.refl \<cdot> TYPE('T5) \<cdot> op \<longrightarrow> \<bullet> prfT5) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.328 +    (impI \<cdot> A \<cdot> C \<bullet> (\<^bold>\<lambda>H: A. iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
   1.329 +      (mp \<cdot> B \<cdot> D \<bullet> prf3 \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> H))))\<close>,
   1.330  
   1.331 -   \<open>(cong % TYPE(bool) % TYPE(bool) % op \<longrightarrow> A % op \<longrightarrow> A % B % C %% prfb %% prfb %%
   1.332 -      (HOL.refl % TYPE(bool=>bool) % op \<longrightarrow> A %% prfbb)) ==
   1.333 -    (cong % TYPE(bool) % TYPE(bool) % op \<longrightarrow> A % op \<longrightarrow> A % B % C %% prfb %% prfb %%
   1.334 -      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.335 -        (op \<longrightarrow> :: bool=>bool=>bool) % (op \<longrightarrow> :: bool=>bool=>bool) % A % A %%
   1.336 -          prfb %% prfbb %%
   1.337 -          (HOL.refl % TYPE(bool=>bool=>bool) % (op \<longrightarrow> :: bool=>bool=>bool) %%
   1.338 -             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.339 -          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.340 +   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op \<longrightarrow> A \<cdot> op \<longrightarrow> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.341 +      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> op \<longrightarrow> A \<bullet> prfbb)) \<equiv>
   1.342 +    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op \<longrightarrow> A \<cdot> op \<longrightarrow> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.343 +      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
   1.344 +        (op \<longrightarrow> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op \<longrightarrow> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
   1.345 +          prfb \<bullet> prfbb \<bullet>
   1.346 +          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op \<longrightarrow> :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
   1.347 +             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
   1.348 +          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
   1.349  
   1.350     (* \<not> *)
   1.351  
   1.352 -   \<open>(iffD1 % \<not> P % \<not> Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%
   1.353 -      (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==
   1.354 -    (notI % Q %% (Lam H: Q.
   1.355 -      notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))\<close>,
   1.356 +   \<open>(iffD1 \<cdot> \<not> P \<cdot> \<not> Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Not \<cdot> Not \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.357 +      (HOL.refl \<cdot> TYPE('T3) \<cdot> Not \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<equiv>
   1.358 +    (notI \<cdot> Q \<bullet> (\<^bold>\<lambda>H: Q.
   1.359 +      notE \<cdot> P \<cdot> False \<bullet> prf2 \<bullet> (iffD2 \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> H)))\<close>,
   1.360  
   1.361 -   \<open>(iffD2 % \<not> P % \<not> Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%
   1.362 -      (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==
   1.363 -    (notI % P %% (Lam H: P.
   1.364 -      notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))\<close>,
   1.365 +   \<open>(iffD2 \<cdot> \<not> P \<cdot> \<not> Q \<bullet> (cong \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Not \<cdot> Not \<cdot> P \<cdot> Q \<bullet> prfT1 \<bullet> prfT2 \<bullet>
   1.366 +      (HOL.refl \<cdot> TYPE('T3) \<cdot> Not \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<equiv>
   1.367 +    (notI \<cdot> P \<bullet> (\<^bold>\<lambda>H: P.
   1.368 +      notE \<cdot> Q \<cdot> False \<bullet> prf2 \<bullet> (iffD1 \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> H)))\<close>,
   1.369  
   1.370     (* = *)
   1.371  
   1.372 -   \<open>(iffD1 % B % D %%
   1.373 -      (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.374 -        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.375 -          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==
   1.376 -    (iffD1 % C % D %% prf2 %%
   1.377 -      (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))\<close>,
   1.378 +   \<open>(iffD1 \<cdot> B \<cdot> D \<bullet>
   1.379 +      (iffD1 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
   1.380 +        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> op = \<cdot> op = \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
   1.381 +          (HOL.refl \<cdot> TYPE('T3) \<cdot> op = \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4) \<equiv>
   1.382 +    (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
   1.383 +      (iffD1 \<cdot> A \<cdot> C \<bullet> prf3 \<bullet> (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf4)))\<close>,
   1.384  
   1.385 -   \<open>(iffD2 % B % D %%
   1.386 -      (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.387 -        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.388 -          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==
   1.389 -    (iffD1 % A % B %% prf1 %%
   1.390 -      (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))\<close>,
   1.391 +   \<open>(iffD2 \<cdot> B \<cdot> D \<bullet>
   1.392 +      (iffD1 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
   1.393 +        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> op = \<cdot> op = \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
   1.394 +          (HOL.refl \<cdot> TYPE('T3) \<cdot> op = \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4) \<equiv>
   1.395 +    (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet>
   1.396 +      (iffD2 \<cdot> A \<cdot> C \<bullet> prf3 \<bullet> (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> prf4)))\<close>,
   1.397  
   1.398 -   \<open>(iffD1 % A % C %%
   1.399 -      (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.400 -        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.401 -          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)==
   1.402 -    (iffD2 % C % D %% prf2 %%
   1.403 -      (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))\<close>,
   1.404 +   \<open>(iffD1 \<cdot> A \<cdot> C \<bullet>
   1.405 +      (iffD2 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
   1.406 +        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> op = \<cdot> op = \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
   1.407 +          (HOL.refl \<cdot> TYPE('T3) \<cdot> op = \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4)\<equiv>
   1.408 +    (iffD2 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet>
   1.409 +      (iffD1 \<cdot> B \<cdot> D \<bullet> prf3 \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf4)))\<close>,
   1.410  
   1.411 -   \<open>(iffD2 % A % C %%
   1.412 -      (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.413 -        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.414 -          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==
   1.415 -    (iffD2 % A % B %% prf1 %%
   1.416 -      (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))\<close>,
   1.417 +   \<open>(iffD2 \<cdot> A \<cdot> C \<bullet>
   1.418 +      (iffD2 \<cdot> A = C \<cdot> B = D \<bullet> (cong \<cdot> TYPE(bool) \<cdot> TYPE('T1) \<cdot> x1 \<cdot> x2 \<cdot> C \<cdot> D \<bullet> prfb \<bullet> prfT1 \<bullet>
   1.419 +        (cong \<cdot> TYPE(bool) \<cdot> TYPE('T2) \<cdot> op = \<cdot> op = \<cdot> A \<cdot> B \<bullet> prfb \<bullet> prfT2 \<bullet>
   1.420 +          (HOL.refl \<cdot> TYPE('T3) \<cdot> op = \<bullet> prfT3) \<bullet> prf1) \<bullet> prf2) \<bullet> prf3) \<bullet> prf4) \<equiv>
   1.421 +    (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet>
   1.422 +      (iffD2 \<cdot> B \<cdot> D \<bullet> prf3 \<bullet> (iffD1 \<cdot> C \<cdot> D \<bullet> prf2 \<bullet> prf4)))\<close>,
   1.423  
   1.424 -   \<open>(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%
   1.425 -      (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) ==
   1.426 -    (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%
   1.427 -      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.428 -        (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%
   1.429 -          prfb %% prfbb %%
   1.430 -          (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %%
   1.431 -             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.432 -          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.433 +   \<open>(cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op = A \<cdot> op = A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.434 +      (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot> op = A \<bullet> prfbb)) \<equiv>
   1.435 +    (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool) \<cdot> op = A \<cdot> op = A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prfb \<bullet>
   1.436 +      (cong \<cdot> TYPE(bool) \<cdot> TYPE(bool\<Rightarrow>bool) \<cdot>
   1.437 +        (op = :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op = :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
   1.438 +          prfb \<bullet> prfbb \<bullet>
   1.439 +          (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> (op = :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
   1.440 +             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
   1.441 +          (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
   1.442  
   1.443     (** transitivity, reflexivity, and symmetry **)
   1.444  
   1.445 -   \<open>(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==
   1.446 -    (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))\<close>,
   1.447 +   \<open>(iffD1 \<cdot> A \<cdot> C \<bullet> (HOL.trans \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prf1 \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.448 +    (iffD1 \<cdot> B \<cdot> C \<bullet> prf2 \<bullet> (iffD1 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf3))\<close>,
   1.449  
   1.450 -   \<open>(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==
   1.451 -    (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))\<close>,
   1.452 +   \<open>(iffD2 \<cdot> A \<cdot> C \<bullet> (HOL.trans \<cdot> TYPE(bool) \<cdot> A \<cdot> B \<cdot> C \<bullet> prfb \<bullet> prf1 \<bullet> prf2) \<bullet> prf3) \<equiv>
   1.453 +    (iffD2 \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> (iffD2 \<cdot> B \<cdot> C \<bullet> prf2 \<bullet> prf3))\<close>,
   1.454  
   1.455 -   \<open>(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf\<close>,
   1.456 +   \<open>(iffD1 \<cdot> A \<cdot> A \<bullet> (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb) \<bullet> prf) \<equiv> prf\<close>,
   1.457  
   1.458 -   \<open>(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf\<close>,
   1.459 +   \<open>(iffD2 \<cdot> A \<cdot> A \<bullet> (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb) \<bullet> prf) \<equiv> prf\<close>,
   1.460  
   1.461 -   \<open>(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)\<close>,
   1.462 +   \<open>(iffD1 \<cdot> A \<cdot> B \<bullet> (sym \<cdot> TYPE(bool) \<cdot> B \<cdot> A \<bullet> prfb \<bullet> prf)) \<equiv> (iffD2 \<cdot> B \<cdot> A \<bullet> prf)\<close>,
   1.463  
   1.464 -   \<open>(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)\<close>,
   1.465 +   \<open>(iffD2 \<cdot> A \<cdot> B \<bullet> (sym \<cdot> TYPE(bool) \<cdot> B \<cdot> A \<bullet> prfb \<bullet> prf)) \<equiv> (iffD1 \<cdot> B \<cdot> A \<bullet> prf)\<close>,
   1.466  
   1.467     (** normalization of HOL proofs **)
   1.468  
   1.469 -   \<open>(mp % A % B %% (impI % A % B %% prf)) == prf\<close>,
   1.470 +   \<open>(mp \<cdot> A \<cdot> B \<bullet> (impI \<cdot> A \<cdot> B \<bullet> prf)) \<equiv> prf\<close>,
   1.471  
   1.472 -   \<open>(impI % A % B %% (mp % A % B %% prf)) == prf\<close>,
   1.473 +   \<open>(impI \<cdot> A \<cdot> B \<bullet> (mp \<cdot> A \<cdot> B \<bullet> prf)) \<equiv> prf\<close>,
   1.474  
   1.475 -   \<open>(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x\<close>,
   1.476 +   \<open>(spec \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> (allI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa \<bullet> prf)) \<equiv> prf \<cdot> x\<close>,
   1.477  
   1.478 -   \<open>(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf\<close>,
   1.479 +   \<open>(allI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa \<bullet> (\<^bold>\<lambda>x::'a. spec \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> prf)) \<equiv> prf\<close>,
   1.480  
   1.481 -   \<open>(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)\<close>,
   1.482 +   \<open>(exE \<cdot> TYPE('a) \<cdot> P \<cdot> Q \<bullet> prfa \<bullet> (exI \<cdot> TYPE('a) \<cdot> P \<cdot> x \<bullet> prfa \<bullet> prf1) \<bullet> prf2) \<equiv> (prf2 \<cdot> x \<bullet> prf1)\<close>,
   1.483  
   1.484 -   \<open>(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf\<close>,
   1.485 +   \<open>(exE \<cdot> TYPE('a) \<cdot> P \<cdot> Q \<bullet> prfa \<bullet> prf \<bullet> (exI \<cdot> TYPE('a) \<cdot> P \<bullet> prfa)) \<equiv> prf\<close>,
   1.486  
   1.487 -   \<open>(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)\<close>,
   1.488 +   \<open>(disjE \<cdot> P \<cdot> Q \<cdot> R \<bullet> (disjI1 \<cdot> P \<cdot> Q \<bullet> prf1) \<bullet> prf2 \<bullet> prf3) \<equiv> (prf2 \<bullet> prf1)\<close>,
   1.489  
   1.490 -   \<open>(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)\<close>,
   1.491 +   \<open>(disjE \<cdot> P \<cdot> Q \<cdot> R \<bullet> (disjI2 \<cdot> Q \<cdot> P \<bullet> prf1) \<bullet> prf2 \<bullet> prf3) \<equiv> (prf3 \<bullet> prf1)\<close>,
   1.492  
   1.493 -   \<open>(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1\<close>,
   1.494 +   \<open>(conjunct1 \<cdot> P \<cdot> Q \<bullet> (conjI \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> prf2)) \<equiv> prf1\<close>,
   1.495  
   1.496 -   \<open>(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2\<close>,
   1.497 +   \<open>(conjunct2 \<cdot> P \<cdot> Q \<bullet> (conjI \<cdot> P \<cdot> Q \<bullet> prf1 \<bullet> prf2)) \<equiv> prf2\<close>,
   1.498  
   1.499 -   \<open>(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1\<close>,
   1.500 +   \<open>(iffD1 \<cdot> A \<cdot> B \<bullet> (iffI \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf2)) \<equiv> prf1\<close>,
   1.501  
   1.502 -   \<open>(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2\<close>];
   1.503 +   \<open>(iffD2 \<cdot> A \<cdot> B \<bullet> (iffI \<cdot> A \<cdot> B \<bullet> prf1 \<bullet> prf2)) \<equiv> prf2\<close>];
   1.504  
   1.505  
   1.506  (** Replace congruence rules by substitution rules **)