Module prop;

(* True *)

$[True:Prop];
$[true:True];

(* And *)

$[And : Prop -> Prop -> Prop];
$[pair : {A,B|Prop}A->B->(And A B)];
$[fst : {A,B|Prop}(And A B) -> A];
$[snd : {A,B|Prop}(And A B) -> B];

[[A,B:Prop][a:A][b:B]
   fst (pair a b) ==> a
|| snd (pair a b) ==> b];


(* False *)

$[False:Prop];
$[falseE : {X:Prop}False -> X];

(* Or *)

$[Or : Prop -> Prop -> Prop];
$[inl : {A,B|Prop}A->(Or A B)];
$[inr : {A,B|Prop}B->(Or A B)];
$[case :  {A,B,X|Prop}(A->X)->(B->X)->(Or A B)->X];

[[A,B,X:Prop][f:A->X][g:B->X][a:A][b:B]
   case f g (inl a) ==> f a
|| case f g (inr b) ==> g b];

(* Definitions *)

[not = [A:Prop]A->False];
[iff = [A,B:Prop]And (A -> B) (B -> A)];
(* to enable /\, \/ *)
[and = And];
[or = Or];