}.
coercion qd.
-(*
+
+(* se togli il D da acin D a non ce la fa ancora *)
inductive iall (D:QD) (P:D \to Prop) : Prop \def
- | iall_intro: (\forall (a:D). acin D a \to P a) \to iall D P.
-*)
+ | iall_intro: (\forall a:D. acin D a \to P a) \to iall D P.