fact: Definition sigma_get A (null : A) (map : sigma A) (n : positive) : A := match PositiveMap.find n map with | None => null | Some x => x end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)