proposition: Lemma pi0_inj: forall i j, pi0 i = pi0 j -> i = j.
proof: Proof. intros. cut (@inl num num i = @inl num num j). intro H'. injection H'. auto. rewrite <- match_pi0, H. apply match_pi0. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)