proposition: Lemma sigT_decompose_eq {A: Type} {B} {x y: {a: A & B a}} {p: x = y}: p = (sigT_eta x) • (= projT1_eq p; projT2_eq p) • (eq_sym (sigT_eta y)).
proof: Proof. now destruct p, x. Qed.
imports: Logic.FunctionalExtensionality Logic.Eqdep_dec Bonak(Notation)