| dall_intro: (∀d. cin ? d → P d) → dall D P
.
-interpretation "internal for all" 'iforall η.x = (dall _ x).
+interpretation "internal for all" 'iforall η.x = (dall ? x).
(* internal existential quantification *)
inductive dex (D:Domain) (P:D → Prop): Prop ≝
| dex_intro: ∀d. cin D d → P d → dex D P
.
-interpretation "internal exists" 'iexists η.x = (dex _ x).
+interpretation "internal exists" 'iexists η.x = (dex ? x).