hbhb bbk
$$ imp(a\ b:Prop):=a\rightarrow b\ . $$
$$ total\ U\ R:=\forall x\ y:U,R\ x\ y\lor R\ y\ x\ . $$
$$ em \ a:=a\lor \lnot a\ . $$
$$ (\forall a,em\ a)\rightarrow total\ imp\ . $$
Require Import Utf8.
Set Implicit Arguments.
Definition imp(a b:Prop):=a → b.
Definition total U R:=∀x y:U,R x y∨R y x.
Definition em a:=a∨¬a.
Goal (∀a,em a) → total imp.
Proof. Abort.