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