X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fsupport%2Fnatural_deduction.ma;h=f5799b90e3a9435a90253876ed4903e42296fc52;hb=5755ebe4016316a474ad8ab8d33b1a1a9187cc9e;hp=9ae03f502df8200fd670e8b8802a74c967545e10;hpb=e189bde1e0a562e8689ff41d55d392431609e749;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 9ae03f502..f5799b90e 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -45,6 +45,21 @@ definition Discharge := λA:CProp.λa:A.
 
 axiom Raa : ∀A.(Not A → Bot) → A.
 
+axiom sort : Type.
+
+inductive Exists (A:Type) (P:A→CProp) : CProp ≝
+  Exists_intro: ∀w:A. P w → Exists A P.
+
+definition Exists_elim ≝
+  λA:Type.λP:A→CProp.λC:CProp.λc:Exists A P.λH:(Πx.P x → C).
+   match c with [ Exists_intro w p ⇒ H w p ].
+
+inductive Forall (A:Type) (P:A→CProp) : CProp ≝
+ Forall_intro: (∀n:A. P n) → Forall A P.
+
+definition Forall_elim ≝
+ λA:Type.λP:A→CProp.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ].
+
 (* Dummy proposition *)
 axiom unit : CProp.
 
@@ -61,7 +76,17 @@ interpretation "Bot" 'Bot = Bot.
 interpretation "Not" 'not a = (Not a).
 notation "✶" non associative with precedence 90 for @{'unit}.
 interpretation "dummy prop" 'unit = unit.
-
+notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20
+for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }.
+notation < "hvbox(\exists ident i break . p)" with precedence 20
+for @{ 'myexists (\lambda ${ident i} : $ty. $p) }.
+interpretation "constructive ex" 'myexists \eta.x = (Exists sort x).
+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).
+ 
 (* Variables *)
 axiom A : CProp.
 axiom B : CProp.
@@ -78,24 +103,20 @@ axiom L : CProp.
 axiom M : CProp.
 axiom N : CProp.
 axiom O : CProp.
-axiom P : CProp.
-axiom Q : CProp.
-axiom R : CProp.
-axiom S : CProp.
-axiom T : CProp.
-axiom U : CProp.
-axiom V : CProp.
-axiom W : CProp.
-axiom X : CProp.
-axiom Y : CProp.
-axiom Z : 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.
 
 (* Every formula user provided annotates its proof:
    `A` becomes `(show A ?)` *)
-definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
+definition show : ΠA.A→A ≝ λA:CProp.λa:A.a.
 
 (* When something does not fit, this daemon is used *)
-axiom cast: ∀A,B:CProp.B → A.
+axiom cast: ΠA,B:CProp.B → A.
 
 (* begin a proof: draws the root *)
 notation > "'prove' p" non associative with precedence 19 
@@ -111,43 +132,6 @@ 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)).
 
-(* already proved lemma *)
-definition Lemma : ∀A.A→A ≝ λA:CProp.λa:A.a.
-
-notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ko_1 $p $H }.
-interpretation "lemma_ko_1" 'lemma_ko_1 p H = 
-  (show p (cast _ _ (Lemma _ H))). 
-
-notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" 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 _ H)))). 
-
-notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ok_1 $p $H }.
-interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H)). 
-interpretation "lemma_ok_11" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H _)). 
-interpretation "lemma_ok_111" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H _ _)). 
-
-notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" 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))). 
-interpretation "lemma_ok_22" 'lemma_ok_2 p H = 
-  (cast _ _ (show p (Lemma _ H _))). 
-interpretation "lemma_ok_22" 'lemma_ok_2 p H = 
-  (cast _ _ (show p (Lemma _ H _ _))). 
-
-notation > "'lem' term 90 p" non associative with precedence 19
-for @{ 'Lemma $p  }.
-interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
-interpretation "lemma OK" 'Lemma p = (Lemma _ p).
-
-
 (* discharging *)
 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
 for @{ 'discharge_ko_1 $a $H }.
@@ -438,22 +422,22 @@ 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\i) \emsp ident H)" with precedence 19
+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)))).
 
-notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
+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))))).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19
+notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) " 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)).
 
-notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19
+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))).
@@ -517,54 +501,346 @@ 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).
 
-(*DOCBEGIN
-Templates for rules:
-
-        apply rule (⇒_i […] (…)).
-
-        apply rule (∧_i (…) (…));
-        	[
-        	|
-        	]
-
-        apply rule (∨_i_l (…)).
-
-        apply rule (∨_i_r (…)).
-
-        apply rule (¬_i […] (…)).
-
-        apply rule (⊤_i).
-
-        apply rule (⇒_e (…) (…));
-        	[
-        	|
-        	]
-
-        apply rule (∧_e_l (…)).
-
-        apply rule (∧_e_r (…)).
-
-        apply rule (∨_e (…) […] (…) […] (…));
-        	[
-        	|
-        	|
-        	]
-
-        apply rule (¬_e (…) (…));
-        	[
-        	|
-        	]
-
-        apply rule (⊥_e (…)).
-
-        apply rule (prove (…)).
-
-        apply rule (RAA […] (…)).
-
-        apply rule (discharge […]).
+(* ∃ 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)))).
+
+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))))).
+
+notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" 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)).
+
+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))).
+
+notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
+for @{'Exists_intro $t (λ_.?) (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 =
+ (Exists_intro sort P t Pt).
+ 
+(* ∃ elimination *)
+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)))).
+
+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))))).
+
+notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" 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)).
+
+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))).
+
+definition ex_concl := λx:CProp.sort → unit → x.
+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 ?)}. 
+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))).
+interpretation "Exists_elim OK" 'Exists_elim 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)))).
+
+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))))).
+
+notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" 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)).
+
+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))).
+
+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))). 
+interpretation "Forall_intro OK" 'Forall_intro P Px =
+  (Forall_intro sort P Px). 
+
+(* ∀ elimination *)
+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)))).
+
+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))))).
+
+notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)" 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)).
+
+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))).
+
+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))). 
+interpretation "Forall_elim OK" 'Forall_elim P t Px =
+  (Forall_elim sort P t Px). 
 
-DOCEND*)
+(* already proved lemma *)
+definition hide_args : ∀A:Type.∀a: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 _ _ _ _ _ _ _).
+
+(* more args crashes the pattern matcher *)
+
+(* already proved lemma, 0 assumptions *)
+definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+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)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))))). 
 
 
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma_ok_1 $p ($H : $_) }.
+interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
+  (show p (Lemma _ H)). 
 
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))). 
 
+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).
+
+
+(* already proved lemma, 1 assumption *)
+definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝ 
+ λA,B:CProp.λf:A⇒B.λa:A.
+  Imply_elim A B f a.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+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)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+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)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))). 
+
+
+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).
+
+(* already proved lemma, 2 assumptions *)
+definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝ 
+ λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
+  Imply_elim B C (Imply_elim A (B⇒C) f a) b.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+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)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+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)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))). 
+
+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).
+
+(* already proved lemma, 3 assumptions *)
+definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝ 
+ λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
+  Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+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)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+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)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+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))). 
+
+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).