TrivialApart A (Aap:=default_apart). Proof. split. - unfold apart,default_apart. apply _. - intros x y;unfold apart,default_apart;split. + intros E. destruct (dec (x=y)). * destruct (false_ne_true E). * trivial. + intros E;destruct (dec (x=y)) as [e|_]. * destruct (E e). * split. Qed.
Require Import HoTT.Classes.interfaces.abstract_algebra.