‚x\"$\/

	 ∀(a : Type) → a