Definition fromcompltodisjoint (X : UU) : compl (coprod X unit) (ii2 tt) -> X. Proof. intros X0. induction X0 as [ t x ]. induction t as [ x0 | u ]. - assumption. - induction u. apply (fromempty (x (idpath (ii2 tt)))). Defined.