proposition: Lemma sigT_decompose {A: Type} {B} {x y: {a: A & B a}} {p q: x = y} {alpha: projT1_eq p = projT1_eq q} {beta: rew [fun r => rew [fun b: A => B b] r in x.2 = y.2] alpha in projT2_eq p = projT2_eq q}: p = q.
proof: Proof. rewrite (sigT_decompose_eq (p := q)), (sigT_decompose_eq (p := p)). destruct x, y; simpl. now destruct beta, alpha. Qed.
imports: Logic.FunctionalExtensionality Logic.Eqdep_dec Bonak(Notation)