proposition: Lemma ext A (B : A -> Type) (f1 f2 : forall x, B x) : f1 = f2 -> forall x, f1 x = f2 x.
proof: Proof. by move=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms)