X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fsupport%2Fnatural_deduction.ma;h=a2e58dd72a8469f2de7f7fce332bc547d9ac756d;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=6c106a2d4ce1b99ff91cdd9cee06be9a953e8481;hpb=f7bfc8096055b1a8e82594b7079bad987676e639;p=helm.git

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 6c106a2d4..a2e58dd72 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -1,3 +1,17 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
 (* Logic system *)
 
 inductive Imply (A,B:CProp) : CProp ≝
@@ -85,7 +99,7 @@ notation > "\forall ident x.break term 19 Px" with precedence 20
 for @{ 'Forall (λ${ident x}.$Px) }.
 notation < "\forall ident x.break term 19 Px" with precedence 20
 for @{ 'Forall (λ${ident x}:$tx.$Px) }.
-interpretation "Forall" 'Forall \eta.Px = (Forall _ Px).
+interpretation "Forall" 'Forall \eta.Px = (Forall ? Px).
  
 (* Variables *)
 axiom A : CProp.
@@ -118,8 +132,8 @@ axiom cast: ΠA,B:CProp.B → A.
 (* begin a proof: draws the root *)
 notation > "'prove' p" non associative with precedence 19 
 for @{ 'prove $p }.
-interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
-interpretation "prove OK" 'prove p = (show p _).
+interpretation "prove KO" 'prove p = (cast ? ? (show p ?)).
+interpretation "prove OK" 'prove p = (show p ?).
 
 (* Leaves *)
 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
@@ -127,402 +141,403 @@ for @{ 'leaf_ok $a $t }.
 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 
 for @{ 'leaf_ko $a $t }.
-interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
+interpretation "leaf KO" 'leaf_ko a t = (cast ? ? (show a t)).
 
 (* discharging *)
 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
 for @{ 'discharge_ko_1 $a $H }.
 interpretation "discharge_ko_1" 'discharge_ko_1 a H = 
-  (show a (cast _ _ (Discharge _ H))).
+  (show a (cast ? ? (Discharge ? H))).
 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19 
 for @{ 'discharge_ko_2 $a $H }.
 interpretation "discharge_ko_2" 'discharge_ko_2 a H = 
-  (cast _ _ (show a (cast _ _ (Discharge _ H)))).
+  (cast ? ? (show a (cast ? ? (Discharge ? H)))).
 
 notation < "[ a ] \sup H" with precedence 19 
 for @{ 'discharge_ok_1 $a $H }.
 interpretation "discharge_ok_1" 'discharge_ok_1 a H = 
-  (show a (Discharge _ H)).
+  (show a (Discharge ? H)).
 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 
 for @{ 'discharge_ok_2 $a $H }.
 interpretation "discharge_ok_2" 'discharge_ok_2 a H = 
-  (cast _ _ (show a (Discharge _ H))).
+  (cast ? ? (show a (Discharge ? H))).
 
 notation > "'discharge' [H]" with precedence 19 
 for @{ 'discharge $H }.
-interpretation "discharge KO" 'discharge H = (cast _ _ (Discharge _ H)).
-interpretation "discharge OK" 'discharge H = (Discharge _ H).
+interpretation "discharge KO" 'discharge H = (cast ? ? (Discharge ? H)).
+interpretation "discharge OK" 'discharge H = (Discharge ? H).
 
 (* ⇒ introduction *)
 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = 
-  (show ab (cast _ _ (Imply_intro _ _ b))).
+  (show ab (cast ? ? (Imply_intro ? ? b))).
 
 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b = 
-  (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
+  (cast ? ? (show ab (cast ? ? (Imply_intro ? ? b)))).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
+notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = 
-  (show ab (Imply_intro _ _ b)).
+  (show ab (Imply_intro ? ? b)).
 
 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = 
-  (cast _ _ (show ab (Imply_intro _ _ b))).
+  (cast ? ? (show ab (Imply_intro ? ? b))).
 
-notation > "⇒_'i' [ident H] term 90 b" with precedence 19
+notation > "⇒#'i' [ident H] term 90 b" with precedence 19
 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
+
 interpretation "Imply_intro KO" 'Imply_intro b pb = 
-  (cast _ (Imply unit b) (Imply_intro _ b pb)).
+  (cast ? (Imply unit b) (Imply_intro ? b pb)).
 interpretation "Imply_intro OK" 'Imply_intro b pb = 
-  (Imply_intro _ b pb).
+  (Imply_intro ? b pb).
 
 (* ⇒ elimination *)
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 for @{ 'Imply_elim_ko_1 $ab $a $b }.
 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = 
-  (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))).
+  (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a)))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 
 for @{ 'Imply_elim_ko_2 $ab $a $b }.
 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = 
-  (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
+  (cast ? ? (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19 
 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = 
-  (show b (Imply_elim _ _ ab a)).
+  (show b (Imply_elim ? ? ab a)).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19 
 for @{ 'Imply_elim_ok_2 $ab $a $b }.
 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = 
-  (cast _ _ (show b (Imply_elim _ _ ab a))).
+  (cast ? ? (show b (Imply_elim ? ? ab a))).
 
-notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 
+notation > "⇒#'e' term 90 ab term 90 a" with precedence 19 
 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
 interpretation "Imply_elim KO" 'Imply_elim ab a = 
-  (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
+  (cast ? ? (Imply_elim ? ? (cast (Imply unit unit) ? ab) (cast unit ? a))).
 interpretation "Imply_elim OK" 'Imply_elim ab a = 
-  (Imply_elim _ _ ab a). 
+  (Imply_elim ? ? ab a). 
 
 (* ∧ introduction *)
 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 
 for @{ 'And_intro_ko_1 $a $b $ab }.
 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = 
-  (show ab (cast _ _ (And_intro _ _ a b))).
+  (show ab (cast ? ? (And_intro ? ? a b))).
 
 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 
 for @{ 'And_intro_ko_2 $a $b $ab }.
 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = 
-  (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
+  (cast ? ? (show ab (cast ? ? (And_intro ? ? a b)))).
 
-notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19 
+notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19 
 for @{ 'And_intro_ok_1 $a $b $ab }.
 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = 
-  (show ab (And_intro _ _ a b)).
+  (show ab (And_intro ? ? a b)).
 
 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19 
 for @{ 'And_intro_ok_2 $a $b $ab }.
 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = 
-  (cast _ _ (show ab (And_intro _ _ a b))).
+  (cast ? ? (show ab (And_intro ? ? a b))).
 
-notation > "∧_'i' term 90 a term 90 b" with precedence 19 
+notation > "∧#'i' term 90 a term 90 b" with precedence 19 
 for @{ 'And_intro (show $a ?) (show $b ?) }.
-interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
-interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
+interpretation "And_intro KO" 'And_intro a b = (cast ? ? (And_intro ? ? a b)).
+interpretation "And_intro OK" 'And_intro a b = (And_intro ? ? a b).
 
 (* ∧ elimination *)
 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
 for @{ 'And_elim_l_ko_1 $ab $a }.
 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = 
-  (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))).
+  (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab)))).
 
 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
 for @{ 'And_elim_l_ko_2 $ab $a }.
 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = 
-  (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
+  (cast ? ? (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab))))).
 
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19 
 for @{ 'And_elim_l_ok_1 $ab $a }.
 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = 
-  (show a (And_elim_l _ _ ab)).
+  (show a (And_elim_l ? ? ab)).
 
 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19 
 for @{ 'And_elim_l_ok_2 $ab $a }.
 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = 
-  (cast _ _ (show a (And_elim_l _ _ ab))).
+  (cast ? ? (show a (And_elim_l ? ? ab))).
 
-notation > "∧_'e_l' term 90 ab" with precedence 19
+notation > "∧#'e_l' term 90 ab" with precedence 19
 for @{ 'And_elim_l (show $ab ?) }.
-interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))).
-interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
+interpretation "And_elim_l KO" 'And_elim_l a = (cast ? ? (And_elim_l ? ? (cast (And unit unit) ? a))).
+interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l ? ? a).
 
 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
 for @{ 'And_elim_r_ko_1 $ab $a }.
 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = 
-  (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))).
+  (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab)))).
 
 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
 for @{ 'And_elim_r_ko_2 $ab $a }.
 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = 
-  (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
+  (cast ? ? (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab))))).
 
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19 
 for @{ 'And_elim_r_ok_1 $ab $a }.
 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = 
-  (show a (And_elim_r _ _ ab)).
+  (show a (And_elim_r ? ? ab)).
 
 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19 
 for @{ 'And_elim_r_ok_2 $ab $a }.
 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = 
-  (cast _ _ (show a (And_elim_r _ _ ab))).
+  (cast ? ? (show a (And_elim_r ? ? ab))).
 
-notation > "∧_'e_r' term 90 ab" with precedence 19
+notation > "∧#'e_r' term 90 ab" with precedence 19
 for @{ 'And_elim_r (show $ab ?) }.
-interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))).
-interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
+interpretation "And_elim_r KO" 'And_elim_r a = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))).
+interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a).
 
 (* ∨ introduction *)
 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
 for @{ 'Or_intro_l_ko_1 $a $ab }.
 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = 
-  (show ab (cast _ _ (Or_intro_l _ _ a))).
+  (show ab (cast ? ? (Or_intro_l ? ? a))).
 
 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
 for @{ 'Or_intro_l_ko_2 $a $ab }.
 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = 
-  (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
+  (cast ? ? (show ab (cast ? ? (Or_intro_l ? ? a)))).
 
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19 
 for @{ 'Or_intro_l_ok_1 $a $ab }.
 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = 
-  (show ab (Or_intro_l _ _ a)).
+  (show ab (Or_intro_l ? ? a)).
 
 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
 for @{ 'Or_intro_l_ok_2 $a $ab }.
 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
-  (cast _ _ (show ab (Or_intro_l _ _ a))).
+  (cast ? ? (show ab (Or_intro_l ? ? a))).
 
-notation > "∨_'i_l' term 90 a" with precedence 19
+notation > "∨#'i_l' term 90 a" with precedence 19
 for @{ 'Or_intro_l (show $a ?) }.
-interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
-interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). 
+interpretation "Or_intro_l KO" 'Or_intro_l a = (cast ? (Or ? unit) (Or_intro_l ? ? a)).
+interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l ? ? a). 
   
 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
 for @{ 'Or_intro_r_ko_1 $a $ab }.
 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = 
-  (show ab (cast _ _ (Or_intro_r _ _ a))).
+  (show ab (cast ? ? (Or_intro_r ? ? a))).
 
 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
 for @{ 'Or_intro_r_ko_2 $a $ab }.
 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = 
-  (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
+  (cast ? ? (show ab (cast ? ? (Or_intro_r ? ? a)))).
 
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19 
 for @{ 'Or_intro_r_ok_1 $a $ab }.
 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = 
-  (show ab (Or_intro_r _ _ a)).
+  (show ab (Or_intro_r ? ? a)).
 
 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 
 for @{ 'Or_intro_r_ok_2 $a $ab }.
 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = 
-  (cast _ _ (show ab (Or_intro_r _ _ a))).
+  (cast ? ? (show ab (Or_intro_r ? ? a))).
 
-notation > "∨_'i_r' term 90 a" with precedence 19
+notation > "∨#'i_r' term 90 a" with precedence 19
 for @{ 'Or_intro_r (show $a ?) }.
-interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
-interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). 
+interpretation "Or_intro_r KO" 'Or_intro_r a = (cast ? (Or unit ?) (Or_intro_r ? ? a)).
+interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r ? ? a). 
 
 (* ∨ elimination *)
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = 
-  (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc)))).
+  (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc)))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = 
-  (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
+  (cast ? ? (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19
 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = 
-  (show c (Or_elim _ _ _ ab ac bc)).
+  (show c (Or_elim ? ? ? ab ac bc)).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = 
-  (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
+  (cast ? ? (show c (Or_elim ? ? ? ab ac bc))).
 
 definition unit_to ≝ λx:CProp.unit → x.
 
-notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
+notation > "∨#'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
 interpretation "Or_elim KO" 'Or_elim ab ac bc = 
-  (cast _ _ (Or_elim _ _ _ 
-    (cast (Or unit unit) _ ab) 
-    (cast (unit_to unit) (unit_to _) ac) 
-    (cast (unit_to unit) (unit_to _) bc))).
-interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc).
+  (cast ? ? (Or_elim ? ? ? 
+    (cast (Or unit unit) ? ab) 
+    (cast (unit_to unit) (unit_to ?) ac) 
+    (cast (unit_to unit) (unit_to ?) bc))).
+interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim ? ? ? ab ac bc).
 
 (* ⊤ introduction *)
 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
 for @{'Top_intro_ko_1}.
 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = 
-  (show _ (cast _ _ Top_intro)).
+  (show ? (cast ? ? Top_intro)).
 
 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
 for @{'Top_intro_ko_2}.
 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 = 
-  (cast _ _ (show _ (cast _ _ Top_intro))).
+  (cast ? ? (show ? (cast ? ? Top_intro))).
 
-notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
+notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 
 for @{'Top_intro_ok_1}.
-interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
+interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro).
 
-notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
+notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 
 for @{'Top_intro_ok_2 }.
-interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
+interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (show ? Top_intro)).
 
-notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
-interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
+notation > "⊤#'i'" with precedence 19 for @{ 'Top_intro }.
+interpretation "Top_intro KO" 'Top_intro = (cast ? ? Top_intro).
 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 
 (* ⊥ introduction *)
 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 
 for @{'Bot_elim_ko_1 $a $b}.
 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = 
-  (show a (Bot_elim _ (cast _ _ b))).
+  (show a (Bot_elim ? (cast ? ? b))).
 
 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19 
 for @{'Bot_elim_ko_2 $a $b}.
 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b = 
-  (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
+  (cast ? ? (show a (Bot_elim ? (cast ? ? b)))).
 
-notation < "\infrule b a (⊥\sub\e)" with precedence 19 
+notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19 
 for @{'Bot_elim_ok_1 $a $b}.
 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = 
-  (show a (Bot_elim _ b)).
+  (show a (Bot_elim ? b)).
 
 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19 
 for @{'Bot_elim_ok_2 $a $b}.
 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b = 
-  (cast _ _ (show a (Bot_elim _ b))).
+  (cast ? ? (show a (Bot_elim ? b))).
 
-notation > "⊥_'e' term 90 b" with precedence 19 
+notation > "⊥#'e' term 90 b" with precedence 19 
 for @{ 'Bot_elim (show $b ?) }.
-interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).  
-interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
+interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim ? (cast ? ? a)).  
+interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim ? a).
 
 (* ¬ introduction *)
 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = 
-  (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
+  (show ab (cast ? ? (Not_intro ? (cast ? ? b)))).
 
 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = 
-  (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
+  (cast ? ? (show ab (cast ? ? (Not_intro ? (cast ? ? b))))).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
+notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = 
-  (show ab (Not_intro _ b)).
+  (show ab (Not_intro ? b)).
 
 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = 
-  (cast _ _ (show ab (Not_intro _ b))).
+  (cast ? ? (show ab (Not_intro ? b))).
 
-notation > "¬_'i' [ident H] term 90 b" with precedence 19
+notation > "¬#'i' [ident H] term 90 b" with precedence 19
 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
-interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
-interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
+interpretation "Not_intro KO" 'Not_intro a = (cast ? ? (Not_intro ? (cast ? ? a))).
+interpretation "Not_intro OK" 'Not_intro a = (Not_intro ? a).
 
 (* ¬ elimination *)
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 
 for @{ 'Not_elim_ko_1 $ab $a $b }.
 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
-  (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
+  (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 
 for @{ 'Not_elim_ko_2 $ab $a $b }.
 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
-  (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
+  (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19 
 for @{ 'Not_elim_ok_1 $ab $a $b }.
 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = 
-  (show b (Not_elim _ ab a)).
+  (show b (Not_elim ? ab a)).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19 
 for @{ 'Not_elim_ok_2 $ab $a $b }.
 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = 
-  (cast _ _ (show b (Not_elim _ ab a))).
+  (cast ? ? (show b (Not_elim ? ab a))).
 
-notation > "¬_'e' term 90 ab term 90 a" with precedence 19
+notation > "¬#'e' term 90 ab term 90 a" with precedence 19
 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 interpretation "Not_elim KO" 'Not_elim ab a = 
-  (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
+  (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))).
 interpretation "Not_elim OK" 'Not_elim ab a = 
-  (Not_elim _ ab a).
+  (Not_elim ? ab a).
 
 (* RAA *)
 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = 
-  (show Pn (cast _ _ (Raa _ (cast _ _ Px)))).
+  (show Pn (cast ? ? (Raa ? (cast ? ? Px)))).
 
 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = 
-  (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
+  (cast ? ? (show Pn (cast ? ? (Raa ? (cast ? ? Px))))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = 
-  (show Pn (Raa _ Px)).
+  (show Pn (Raa ? Px)).
 
 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = 
-  (cast _ _ (show Pn (Raa _ Px))).
+  (cast ? ? (show Pn (Raa ? Px))).
 
 notation > "'RAA' [ident H] term 90 b" with precedence 19 
 for @{ 'Raa (λ${ident H}.show $b ?) }. 
-interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))).
-interpretation "RAA OK" 'Raa p = (Raa _ p).
+interpretation "RAA KO" 'Raa p = (cast ? unit (Raa ? (cast ? (unit_to ?) p))).
+interpretation "RAA OK" 'Raa p = (Raa ? p).
 
 (* ∃ introduction *)
 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
 for @{ 'Exists_intro_ko_1 $Pn $Px }.
 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px = 
-  (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn)))).
+  (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn)))).
 
 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
 for @{ 'Exists_intro_ko_2 $Pn $Px }.
 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px = 
-  (cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))).
+  (cast ? ? (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn))))).
 
-notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
 for @{ 'Exists_intro_ok_1 $Pn $Px }.
 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px = 
-  (show Px (Exists_intro _ _ _ Pn)).
+  (show Px (Exists_intro ? ? ? Pn)).
 
 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
 for @{ 'Exists_intro_ok_2 $Pn $Px }.
 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px = 
-  (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
+  (cast ? ? (show Px (Exists_intro ? ? ? Pn))).
 
-notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
+notation >"∃#'i' {term 90 t} term 90 Pt" non associative with precedence 19
 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}. 
 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
- (cast _ _ (Exists_intro sort P t (cast _ _ Pt))).
+ (cast ? ? (Exists_intro sort P t (cast ? ? Pt))).
 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
  (Exists_intro sort P t Pt).
  
@@ -530,62 +545,62 @@ interpretation "Exists_intro OK" 'Exists_intro t P Pt =
 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
-    (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc)))).
+    (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc)))).
 
 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
-    (cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))).
+    (cast ? ? (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc))))).
 
-notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
+notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
-    (show c (Exists_elim _ _ _ ExPx Pc)).
+    (show c (Exists_elim ? ? ? ExPx Pc)).
 
 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
-    (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))).
+    (cast ? ? (show c (Exists_elim ? ? ? ExPx Pc))).
 
 definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
 definition ex_concl_dummy := ∀y:sort.unit → unit.
 definition fake_pred := λx:sort.unit.
 
-notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
+notation >"∃#'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
- (cast _ _ (Exists_elim sort P _ 
-   (cast (Exists _ P)  _ ExPt) 
-   (cast ex_concl_dummy (ex_concl _) c))).
+ (cast ? ? (Exists_elim sort P ? 
+   (cast (Exists ? P)  ? ExPt) 
+   (cast ex_concl_dummy (ex_concl ?) c))).
 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
- (Exists_elim sort P _ ExPt c).
+ (Exists_elim sort P ? ExPt c).
 
 (* ∀ introduction *)
 
 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn = 
-  (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px)))).
+  (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px)))).
 
 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn = 
-  (cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))).
+  (cast ? ? (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px))))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn = 
-  (show Pn (Forall_intro _ _ Px)).
+  (show Pn (Forall_intro ? ? Px)).
 
 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn = 
-  (cast _ _ (show Pn (Forall_intro _ _ Px))).
+  (cast ? ? (show Pn (Forall_intro ? ? Px))).
 
-notation > "∀_'i' {ident y} term 90 Px" non associative with precedence 19
+notation > "∀#'i' {ident y} term 90 Px" non associative with precedence 19
 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }. 
 interpretation "Forall_intro KO" 'Forall_intro P Px =
-  (cast _ _ (Forall_intro sort P (cast _ _ Px))). 
+  (cast ? ? (Forall_intro sort P (cast ? ? Px))). 
 interpretation "Forall_intro OK" 'Forall_intro P Px =
   (Forall_intro sort P Px). 
 
@@ -593,41 +608,41 @@ interpretation "Forall_intro OK" 'Forall_intro P Px =
 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 for @{ 'Forall_elim_ko_1 $Px $Pn }.
 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn = 
-  (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px)))).
+  (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px)))).
 
 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 for @{ 'Forall_elim_ko_2 $Px $Pn }.
 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn = 
-  (cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))).
+  (cast ? ? (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px))))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
 for @{ 'Forall_elim_ok_1 $Px $Pn }.
 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn = 
-  (show Pn (Forall_elim _ _ _ Px)).
+  (show Pn (Forall_elim ? ? ? Px)).
 
 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
 for @{ 'Forall_elim_ok_2 $Px $Pn }.
 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn = 
-  (cast _ _ (show Pn (Forall_elim _ _ _ Px))).
+  (cast ? ? (show Pn (Forall_elim ? ? ? Px))).
 
-notation > "∀_'e' {term 90 t} term 90 Pn" non associative with precedence 19
+notation > "∀#'e' {term 90 t} term 90 Pn" non associative with precedence 19
 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }. 
 interpretation "Forall_elim KO" 'Forall_elim P t Px =
-  (cast _ unit (Forall_elim sort P t (cast _ _ Px))). 
+  (cast ? unit (Forall_elim sort P t (cast ? ? Px))). 
 interpretation "Forall_elim OK" 'Forall_elim P t Px =
   (Forall_elim sort P t Px). 
 
 (* already proved lemma *)
-definition hide_args : ∀A:Type.∀a:A.A := λA:Type.λa:A.a.
+definition hide_args : ∀A:Type.A→A := λA:Type.λa:A.a.
 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
-interpretation "hide 0 args"  'hide_args t = (hide_args _ t).
-interpretation "hide 1 args"  'hide_args t = (hide_args _ t _).
-interpretation "hide 2 args"  'hide_args t = (hide_args _ t _ _).
-interpretation "hide 3 args"  'hide_args t = (hide_args _ t _ _ _).
-interpretation "hide 4 args"  'hide_args t = (hide_args _ t _ _ _ _). 
-interpretation "hide 5 args"  'hide_args t = (hide_args _ t _ _ _ _ _).
-interpretation "hide 6 args"  'hide_args t = (hide_args _ t _ _ _ _ _ _).
-interpretation "hide 7 args"  'hide_args t = (hide_args _ t _ _ _ _ _ _ _).
+interpretation "hide 0 args"  'hide_args t = (hide_args ? t).
+interpretation "hide 1 args"  'hide_args t = (hide_args ? t ?).
+interpretation "hide 2 args"  'hide_args t = (hide_args ? t ? ?).
+interpretation "hide 3 args"  'hide_args t = (hide_args ? t ? ? ?).
+interpretation "hide 4 args"  'hide_args t = (hide_args ? t ? ? ? ?). 
+interpretation "hide 5 args"  'hide_args t = (hide_args ? t ? ? ? ? ?).
+interpretation "hide 6 args"  'hide_args t = (hide_args ? t ? ? ? ? ? ?).
+interpretation "hide 7 args"  'hide_args t = (hide_args ? t ? ? ? ? ? ? ?).
 
 (* more args crashes the pattern matcher *)
 
@@ -642,7 +657,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma_ko_1 $p ($H : $_) }.
 interpretation "lemma_ko_1" 'lemma_ko_1 p H = 
-  (show p (cast _ _ (Lemma _ (cast _ _ H)))). 
+  (show p (cast ? ? (Lemma ? (cast ? ? H)))). 
 
 notation < "\infrule 
          (\infrule 
@@ -652,8 +667,8 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma_ko_2 $p ($H : $_) }.
 interpretation "lemma_ko_2" 'lemma_ko_2 p H = 
-  (cast _ _ (show p (cast _ _ 
-    (Lemma _ (cast _ _ H))))). 
+  (cast ? ? (show p (cast ? ? 
+    (Lemma ? (cast ? ? H))))). 
 
 
 notation < "\infrule 
@@ -664,7 +679,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma_ok_1 $p ($H : $_) }.
 interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H)). 
+  (show p (Lemma ? H)). 
 
 notation < "\infrule 
          (\infrule 
@@ -674,13 +689,13 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma_ok_2 $p ($H : $_) }.
 interpretation "lemma_ok_2" 'lemma_ok_2 p H = 
-  (cast _ _ (show p (Lemma _ H))). 
+  (cast ? ? (show p (Lemma ? H))). 
 
 notation > "'lem' 0 term 90 l" non associative with precedence 19
 for @{ 'Lemma (hide_args ? $l : ?) }.
 interpretation "lemma KO" 'Lemma l = 
-  (cast _ _ (Lemma unit (cast unit _ l))). 
-interpretation "lemma OK" 'Lemma l = (Lemma _ l).
+  (cast ? ? (Lemma unit (cast unit ? l))). 
+interpretation "lemma OK" 'Lemma l = (Lemma ? l).
 
 
 (* already proved lemma, 1 assumption *)
@@ -696,7 +711,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H = 
-  (show p (cast _ _ (Lemma1 _ _ (cast _ _ H) (cast _ _ a)))). 
+  (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))). 
 
 notation < "\infrule 
          (\infrule 
@@ -706,8 +721,8 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H = 
-  (cast _ _ (show p (cast _ _ 
-    (Lemma1 _ _ (cast _ _ H) (cast _ _ a))))). 
+  (cast ? ? (show p (cast ? ? 
+    (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))). 
 
 
 notation < "\infrule 
@@ -718,7 +733,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H = 
-  (show p (Lemma1 _ _ H a)). 
+  (show p (Lemma1 ? ? H a)). 
 
 notation < "\infrule 
          (\infrule 
@@ -728,14 +743,14 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H = 
-  (cast _ _ (show p (Lemma1 _ _ H a))). 
+  (cast ? ? (show p (Lemma1 ? ? H a))). 
 
 
 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
 interpretation "lemma 1 KO" 'Lemma1 l p = 
-  (cast _ _ (Lemma1 unit unit (cast (Imply unit unit) _ l) (cast unit _ p))). 
-interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 _ _ l p).
+  (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))). 
+interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p).
 
 (* already proved lemma, 2 assumptions *)
 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝ 
@@ -750,7 +765,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H = 
-  (show p (cast _ _ (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b)))). 
+  (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))). 
 
 notation < "\infrule 
          (\infrule 
@@ -760,8 +775,8 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H = 
-  (cast _ _ (show p (cast _ _ 
-    (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b))))). 
+  (cast ? ? (show p (cast ? ? 
+    (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))). 
 
 
 notation < "\infrule 
@@ -772,7 +787,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H = 
-  (show p (Lemma2 _ _ _ H a b)). 
+  (show p (Lemma2 ? ? ? H a b)). 
 
 notation < "\infrule 
          (\infrule 
@@ -782,13 +797,13 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H = 
-  (cast _ _ (show p (Lemma2 _ _ _ H a b))). 
+  (cast ? ? (show p (Lemma2 ? ? ? H a b))). 
 
 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
 interpretation "lemma 2 KO" 'Lemma2 l p q = 
-  (cast _ _ (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) _ l) (cast unit _ p) (cast unit _ q))). 
-interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 _ _ _ l p q).
+  (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))). 
+interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q).
 
 (* already proved lemma, 3 assumptions *)
 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝ 
@@ -803,8 +818,8 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H = 
-  (show p (cast _ _ 
-   (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c)))). 
+  (show p (cast ? ? 
+   (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))). 
 
 notation < "\infrule 
          (\infrule 
@@ -814,8 +829,8 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H = 
-  (cast _ _ (show p (cast _ _ 
-    (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c))))). 
+  (cast ? ? (show p (cast ? ? 
+    (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))). 
 
 
 notation < "\infrule 
@@ -826,7 +841,7 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H = 
-  (show p (Lemma3 _ _ _ _ H a b c)). 
+  (show p (Lemma3 ? ? ? ? H a b c)). 
 
 notation < "\infrule 
          (\infrule 
@@ -836,10 +851,10 @@ notation < "\infrule
 non associative with precedence 19
 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H = 
-  (cast _ _ (show p (Lemma3 _ _ _ _ H a b c))). 
+  (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))). 
 
 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
 interpretation "lemma 3 KO" 'Lemma3 l p q r = 
-  (cast _ _ (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) _ l) (cast unit _ p) (cast unit _ q) (cast unit _ r))). 
-interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 _ _ _ _ l p q r).
+  (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))). 
+interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r).