proposition: Lemma hpiT_decompose {A: Type} (B: A -> HSet) (f g: forall a: A, B a) (p: f = g): functional_extensionality_dep_good _ _ (fun x => f_equal (fun H => H x) p) = p.
proof: Proof. destruct p; simpl; now apply functional_extensionality_dep_good_refl. Qed.
imports: Logic.FunctionalExtensionality Logic.Eqdep_dec Bonak(Notation)