...

[helm.git] / helm / software / matita / library / didactic / support / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index f5799b90e3a9435a90253876ed4903e42296fc52..6c106a2d4ce1b99ff91cdd9cee06be9a953e8481 100644 (file)
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -103,13 +103,10 @@ axiom L : CProp.
 axiom M : CProp.
 axiom N : CProp.
 axiom O : CProp.
-axiom P : sort →CProp.
-axiom Q : sort →CProp.
-axiom R : sort →sort →CProp.
-axiom S : sort →sort →CProp.
-axiom f : sort → sort.
-axiom g : sort → sort.
-axiom h : sort → sort → sort.
+axiom  x: sort.
+axiom  y: sort.
+axiom  z: sort.
+axiom  w: sort.
 
 (* Every formula user provided annotates its proof:
    `A` becomes `(show A ?)` *)
@@ -523,7 +520,7 @@ interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
   (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
 
 notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
-for @{'Exists_intro $t (λ_.?) (show $Pt ?)}. 
+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))).
 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
@@ -550,14 +547,16 @@ 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))).
 
-definition ex_concl := λx:CProp.sort → unit → x.
+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
-for @{'Exists_elim (λ_.?) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
+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 unit) (ex_concl _) c))).
+   (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).