proposition: Theorem curve_pelt_irr x1 x2 y1 y2 z1 z2 e1 e2 : x1 = x2 -> y1 = y2 -> z1 = z2 -> @mk_pelt x1 y1 z1 e1 = @mk_pelt x2 y2 z2 e2.
proof: Proof. move=> x1E y1E z1E; subst x1 y1 z1. congr mk_pelt. apply: Eqdep_dec.eq_proofs_unicity => x y. by case: (x =P y); [left | right]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)