proposition: Theorem curve_pelt_irr: forall x1 x2 y1 y2 z1 z2 H1 H2, x1 = x2 -> y1 = y2 -> z1 = z2 -> @mk_pelt x1 y1 z1 H1 = @mk_pelt x2 y2 z2 H2.
proof: Proof. intros x1 x2 y1 y2 z1 z2 H1 H2 H3 H4 H5. subst. rewrite (fun H => eq_proofs_unicity H H1 H2); auto. intros x1 y1; case (x1 ?= y1); auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith