o : Type.
conj : o -> o -> Type.
[x : o] conj x x --> conj x x.