proposition: Lemma exist_pi: forall (A:Type) (P: A -> Prop), (forall a (H1 H2:P a), H1=H2) -> forall a H1 H2, exist P a H1 = exist P a H2.
proof: Proof. intros. rewrite (H a H1 H2). reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)