proposition: Lemma sig_rewrite : ∀ {T A} {P : A → Prop} {x y} (p : T → A) (h : P (p x)) (e : x = y), exist _ (p x) h = exist _ (p y) (sig_rewrite_aux p h e).
proof: Proof. intros T A P x y p h e. subst. reflexivity. Qed.
imports: Coq(Utf8 Lia) mathcomp(ssreflect eqtype ssrbool ssrnat) extructures(ord fset) Equations(Equations)