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 ?)` *)
(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 =
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).