*)
definition DBool: Domain ≝
- mk_Domain (mk_Class bool (true_f ?) (eq ?)).
+ mk_Domain (
+ mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+ ).
(*
definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
\lambda C,c0,c1,b.
].
*)
definition DVoid: Domain ≝
- mk_Domain (mk_Class void (true_f ?) (eq ?)).
+ mk_Domain (
+ mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+ ).
(*
definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
\lambda C,v.