proposition: Lemma Equiv_iff eq_elt (m0 m1 : t elt) : Equiv eq_elt m0 m1 <-> PositiveMap.Equiv eq_elt m0 m1.
proof: Proof. unfold Equiv, PositiveMap.Equiv, In, PositiveMap.In; t. Qed.
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.FSets.FMapInterface Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.Prod