+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)))).
+
+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 < "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)).
+
+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 (λ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 =
+ (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 < "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)).
+
+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: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 (λ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))).
+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 < "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)).
+
+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 < "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)).
+
+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).
+
+(* already proved lemma *)
+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 ? ? ? ? ? ? ?).
+
+(* 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).