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