proposition: Lemma sig_eq_intro {n:nat} (x y : t n) : proj1_sig x = proj1_sig y -> x = y.
proof: Proof. destruct x, y; simpl; f_equal; intro; subst. f_equal; apply eq_proofs_unicity_on. destruct y, (x0 <? n); auto. right; discriminate. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)