(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/connectives/".
+set "baseuri" "cic:/matita/logic/connectives/".
inductive True: Prop \def
I : True.
-default "true" cic:/matita/logic/True.ind.
+default "true" cic:/matita/logic/connectives/True.ind.
inductive False: Prop \def .
-default "false" cic:/matita/logic/False.ind.
+default "false" cic:/matita/logic/connectives/False.ind.
definition Not: Prop \to Prop \def
\lambda A. (A \to False).
intros. elim (H1 H).
qed.
-default "absurd" cic:/matita/logic/absurd.ind.
+default "absurd" cic:/matita/logic/connectives/absurd.con.
inductive And (A,B:Prop) : Prop \def
conj : A \to B \to (And A B).