1
(* Test of inference of elimination predicate for "if" *)
2
(* submitted by Robert R Schneck *)
4
Axiom bad : false = true.
6
Definition try1 : False :=
7
match bad in (_ = b) return (if b then False else True) with
11
Definition try2 : False :=
12
match bad in (_ = b) return ((if b then False else True):Prop) with
16
Definition try3 : False :=
18
bad in (_ = b) return ((fun b' : bool => if b' then False else True) b)