{B : Type} `{!IsHSet B} (a : (forall i, A i) -> B) (E : forall (f f' : forall i, A i), (forall i, R i (f i) (f' i)) -> a f = a f') (f : forall i, A i) : choose_quotient_rec a E (fun i => class_of (R i) (f i)) = a f. Proof. apply (choose_quotient_ind_compute (fun _ => B)). Qed.
Require Import