+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).