(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/datatypes/bool/".
-
include "logic/equality.ma".
include "higher_order_defs/functions.ma".
change with
match true with
[ true \Rightarrow False
-| flase \Rightarrow True].
+| false \Rightarrow True].
rewrite > H.simplify.exact I.
qed.
rewrite > H.
rewrite > H1.
reflexivity.
-qed.
\ No newline at end of file
+qed.